19:28 Вывод на знаниях | |
Семантика исчисления предикатов обеспечивает основу для формализации логического вывода. Возможность логически выводить новые правильные выражения из набора истинных утверждений очень важна. Логически выведенные утверждения корректны, и они совместимы со всеми предыдущими интерпретациями первоначального набора выражений. Обсудим вышесказанное неформально и затем введем необходимую формализацию. В исчислении высказываний основным
объектом является переменное высказывание (предикат), истинность или ложность
которого зависит от значений входящих в него переменных. Так, истинность
предиката "x был физиком" зависит от значения
переменной x. Если x
- П. Капица, то предикат истинен, если x - М.
Лермонтов, то он ложен. На языке исчисления предикатов утверждение В исчислении предикатов имеется множество правил вывода. В качестве примера приведем классическое правило отделения, или modus ponens : (A, A B) / B
которое читается так "если истинна формула A и истинно, что из A следует B, то истинна и формула B". Формулы, находящиеся над чертой, называются посылками вывода, а под чертой - заключением. Это правило вывода формализует основной закон дедуктивных систем: из истинных посылок всегда следуют истинные заключения. Аксиомы и правила вывода исчисления предикатов первого порядка задают основу формальной дедуктивной системы, в которой происходит формализация схемы рассуждений в логическом программировании. Можно упомянуть и другие правила вывода. Modus tollendo tollens : Если из A следует B и B ложно, то и A ложно. Modus ponendo tollens : Если A и B не могут одновременно быть истинными и A истинно, то B ложно. Modus tollendo ponens : Если либо A, либо B является истинным и A не истинно, то B истинно. Решаемая задача представляется в виде утверждений (аксиом) f1, F2... Fn исчисления предикатов первого порядка. Цель задачи B также записывается в виде утверждения, справедливость которого следует установить или опровергнуть на основании аксиом и правил вывода формальной системы. Тогда решение задачи (достижение цели задачи) сводится к выяснению логического следования (выводимости) целевой формулы B из заданного множества формул (аксиом) f1, F2... Fn. Такое выяснение равносильно доказательству общезначимости (тождественно-истинности) формулы f1& F2&... & Fn B
или невыполнимости (тождественно-ложности) формулы f1& F2&... & Fn& ¬B
Из практических соображений удобнее использовать доказательство от противного, то есть доказывать невыполнимость формулы. На доказательстве от противного основано и ведущее правило вывода, используемое в логическом программировании, - принцип резолюции. Робинсон открыл более сильное правило вывода, чем modus ponens, которое он назвал принципом резолюции (или правилом резолюции). При использовании принципа резолюции формулы исчисления предикатов с помощью несложных преобразований приводятся к так называемой дизъюнктивной форме, то есть представляются в виде набора дизъюнктов. При этом под дизъюнктом понимается дизъюнкция литералов, каждый из которых является либо предикатом, либо отрицанием предиката. Приведем пример дизъюнкта:
Пусть P - предикат уважать, c1 - Ключевский, Q - предикат знать,c2 - история. Теперь данный дизъюнкт отражает факт "каждый, кто знает историю, уважает Ключевского". Приведем еще один пример дизъюнкта:
Пусть P - предикат знать, c1 - физика, c2 - история. Данный дизъюнкт отражает запрос "кто знает физику и историю одновременно". Таким образом, условия решаемых
задач (факты) и целевые утверждения задач (запросы) можно выразить в
дизъюнктивной форме логики предикатов первого порядка. В дизъюнктах кванторы всеобщности
| |
|
Всего комментариев: 0 | |
Информер последних комментариев
21:41, 06.11.2016
20:21, 10.10.2015
14:24, 30.03.2014
14:23, 30.03.2014
19:31, 13.03.2014
19:28, 13.03.2014
19:39, 10.03.2014
18:19, 16.02.2014
16:34, 16.02.2014
11:37, 04.01.2014