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С

Правило резолюции для исчисления предикатов.

Другими словами, при применении правила резолюции нужны контрарные литералы в резольвируемых предложениях. Пусть С₁ и С₂ - два предложения в исчислении предикатов. Правило вывода

называется правилом резолюции в исчислении предикатов, если в предложениях С₁ и С₂ существуют унифицируемые контрарные литералы P₁ и P₂, то есть C₁ = P₁  и C₂ = P₁ , причем атомарные формулы P₁ и P₂ являются унифицируемыми наиболее общим унификатором .В этом случае резольвентой предложений C₁ и C₂ является предложение (  ), полученное из предложения  применением унификатора .

Опровержение методом резолюций.

Опровержение методом резолюций – это алгоритм автоматического доказательства теорем в прикладном исчислении предикатов, который сводится к следующему. Пусть нужно установить выводимость

S├ G.

Каждая формула множества S и формула G (отрицание целевой теоремы) независимо преобразуются в множества предложений. В полученном совокупном множестве предложений C отыскиваются резольвируемые предложения, к ним применяется правило резолюций и резольвента добавляется в множество до тех пор, пока не будет получено пустое предложение. При этом возможны три случая:

1. Среди текущего множества предложений нет резольвируемых. Это означает, что теорема опровергнута, то есть формула G не выводима из множества формул S.

2. В результате очередного применения правила резолюции получено пустое предложение. Это означает, что теорема доказана. то есть S├ G.

Процесс не заканчивается, то есть множество предложений пополняется все новыми резольвентами, среди которых нет пустых. Это ничего не означает.

6.4 Принцип логического программирования.

Далее вставка 6D

1. Формы представления логических формул.

Далее вставка 6E1-6E2

6.5 Вопросы для самопроверки.

1) Что такое исчисление предикатов?

2) Дать основные понятия исчисления предикатов.

3) В чем заключается метод резолюции в логике высказываний и в логике предикатов?

4) Чем отличается логика высказываний от логики предикатов?

5) Записать на языке предикатов:

а) все аспиранты учатся;

б) некоторые спортсмены отличники;

в) для любого числа можно найти большее число.

Характеристики

Список файлов книги