6_ исчисление предикатов (1019124), страница 2
Текст из файла (страница 2)
3. x (A(x) & B(x)) x A(x) & x B(x), x A(x) x B(x) x (A(x) B(x)),
4. x y A(x, y) = y x A(x, y), x y A(x, y) = y x A(x, y),
5. x (A(x) & C) = x A(x) & C, x (A(x) C) = x A(x) C,
6. x (A(x) & C) = x A(x) & C, x (A(x) C) = x A(x) C,
7. C x A(x) = x (C A(x)), C x A(x) = x (C A(x)),
8. x A(x) C x (A(x) C), x A(x) C x (A(x) C)
где формула С не содержит никаких вхождений переменной x.
Для всякой формулы А существует логически эквивалентная ей формула А’ в предваренной форме:
где - некоторые кванторы, а
- бескванторная формула.
6.3 Метод резолюции в логике предикатов.
Далее вставка 6С
Правило резолюции для исчисления предикатов.
Другими словами, при применении правила резолюции нужны контрарные литералы в резольвируемых предложениях. Пусть С1 и С2 - два предложения в исчислении предикатов. Правило вывода
называется правилом резолюции в исчислении предикатов, если в предложениях С1 и С2 существуют унифицируемые контрарные литералы P1 и P2, то есть C1 = P1 и C2 = P1
, причем атомарные формулы P1 и P2 являются унифицируемыми наиболее общим унификатором .В этом случае резольвентой предложений C1 и C2 является предложение (
), полученное из предложения
применением унификатора .
Опровержение методом резолюций.
Опровержение методом резолюций – это алгоритм автоматического доказательства теорем в прикладном исчислении предикатов, который сводится к следующему. Пусть нужно установить выводимость
S├ G.
Каждая формула множества S и формула G (отрицание целевой теоремы) независимо преобразуются в множества предложений. В полученном совокупном множестве предложений C отыскиваются резольвируемые предложения, к ним применяется правило резолюций и резольвента добавляется в множество до тех пор, пока не будет получено пустое предложение. При этом возможны три случая:
-
Среди текущего множества предложений нет резольвируемых. Это означает, что теорема опровергнута, то есть формула G не выводима из множества формул S.
-
В результате очередного применения правила резолюции получено пустое предложение. Это означает, что теорема доказана. то есть S├ G.
Процесс не заканчивается, то есть множество предложений пополняется все новыми резольвентами, среди которых нет пустых. Это ничего не означает.
6.4 Принцип логического программирования.
Далее вставка 6D
-
Формы представления логических формул.
Далее вставка 6E1-6E2
6.5 Вопросы для самопроверки.
1) Что такое исчисление предикатов?
2) Дать основные понятия исчисления предикатов.
3) В чем заключается метод резолюции в логике высказываний и в логике предикатов?
4) Чем отличается логика высказываний от логики предикатов?
5) Записать на языке предикатов:
а) все аспиранты учатся;
б) некоторые спортсмены отличники;
в) для любого числа можно найти большее число.