Средства разработки приложений
Элиминируем кванторы всеобщности. Полученная формула
Третий шаг. Элиминируем кванторы всеобщности. Полученная формула будет бескванторной и эквивалентной исходной в смысле выполнимости.
Четвертый шаг. Приведем формулу к конъюнктивной нормальной форме, для чего воспользуемся эквивалентностями, выражающими дистрибутивность:
A ∨ (B ∧ C) ≡ (A ∨ B) ∧ (A ∨ C) A ∧ (B ∨ C) ≡ (A ∧ B) ∨ (A ∧ C) Пятый шаг. Элиминируем конъюнкции, представляя формулу в виде множества дизъюнктов.
Получаем множество дизъюнктов, эквивалентное исходной формуле в том смысле, который дает нам следующая теорема.
Теорема. Формула является тождественно ложной тогда и только тогда, когда множество дизъюнктов, полученных из нее, является невыполнимым.
Напомним, что множество формул называется невыполнимым, если не существует такого означивания переменных, чтобы все формулы из этого множества были бы истинными.
Пример. Превратим формулу ∀x(P(x) → ∃y(P(y) ∨ ¬Q(x,y))) в эквивалентное ей множество дизъюнктов.
Первый шаг. Приведем исходную формулу к предваренной нормальной форме. Элиминировав импликацию, получим формулу ∀x(¬P(x) ∨ ∃y(P(y) ∨ ¬Q(x,y))). Вынесем переменную y за скобки: ∀x∃y(¬P(x) ∨ (P(y) ∨ ¬Q(x,y))). Это можно сделать, потому что формула ¬P(x) не зависит от переменной y. Если бы она зависела, то можно было бы переименовать связанную переменную y.
Второй шаг. Проведем сколемизацию полученной формулы. Левее квантора существования стоит квантор всеобщности, значит, нужно заменить все вхождения переменной y новым унарным функциональным символом, зависящим от x. Получим формулу, находящуюся в сколемовской нормальной форме: ∀x(¬P(x) ∨ (P(f(x) ∨ ¬Q(x,f(x)))).
Третий шаг. Элиминируем квантор всеобщности: ¬P(x) ∨ (P(f(x)) ∨ ¬Q(x,f(x))).
В четвертом и пятом шагах необходимости нет, поскольку формула уже представляет собой дизъюнкт: ¬P(x) ∨ P(f(x)) ∨ ¬Q(x,f(x)).
Следующая техника, лежащая в основе Пролога, с которой мы попробуем разобраться, — это унификация. Унификация позволяет отождествлять формулы логики первого порядка путем замены свободных переменных на термы.
Forekc.ru
Рефераты, дипломы, курсовые, выпускные и квалификационные работы, диссертации, учебники, учебные пособия, лекции, методические пособия и рекомендации, программы и курсы обучения, публикации из профильных изданий