Курсовая работа: Принцип резолюции в исчислении высказываний и логике предикатов и его модификации

ф= {ф1..., фi.....,фn}, и

Ui, = ¬фi при 1[i[mm,1 [j [ n,

то новую фразу £ можно вывести из объединения U' и ф', где

U' = U¬{ Ui} и ф' = ф¬{ф,}.

Фраза £ = U' и ф' называется резольвентой шага резолюции, а U и ф являются родительскими фразами. Иногда говорят, что U и ф "сталкиваются" на паре дополняющих литералов Ui , и фj.

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

В левой колонке табл. 1 перечислены наименования правил вывода, в средней показано, как они выглядят в обычных обозначениях, а в правой колонке — во фразовой форме. В каждой записи выражения в верхней части представляют схему предпосылок, а выражения в нижней части — схему заключений. Из этой таблицы видно, что каждое из цитированных выше пяти правил является одним из экземпляров резолюции:

Таблица 1 . Обобщение резолюции.

Правило вывода	Обычная форма	Конъюнктивная нормальная форма
Modus ponens	(Uф,U)/Ф	{¬U,Ф},{U}/{ф}
Modus fallens	(Uф.¬ф)/-U	{¬U,ф},{-,ф}/{-U}
Сцепление	(Uф,ф£)(U£)	{¬U,ф},{¬ф,£}/{¬U,£}
Слияние	(Uф,¬U ф)/ф	{U,ф},{¬U,ф}/{ф}
Reductio	(U,¬U)/ |	{¬U},{U}/{}

Противоречие в правиле, которое обычно обозначается значком 1, дает в результате пустую фразу— {}. Это означает, что предпосылки несовместимы. Если считать, что предпосылки описывают некоторое состояние предметной области, то такой набор предпосылок не может быть реально обеспечен в ней, т.е. такое состояние невозможно.

Главное, что компонент автоматического доказательства теорем, который является основным компонентом большинства систем искусственного интеллекта и, в частности, языков программирования искусственного интеллекта, таких как PROLOG, является системой, опровержения резолюций. Для того чтобы доказать, что р следует из некоторого описания состояния (или теории) Т, нужно положить —р и попытаться доказать, что из этого предположения следует утверждение, противоречащее Т. Если это удастся сделать, то тем самым подтверждается утверждение р, а в противном случае оно опровергается.

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

Например, выражения БЕЖИТ_БЫСТРЕЕ_ЧЕМ(Х, улитка) и БЕЖИТ_БЫСТРЕЕ _ЧЕМ (черепаха, Y) превращаются в идентичные при подстановке {Х/черепаха, Y/улитка}. Такая подстановка называется унификатором. Наша цель — отыскать наиболее общую подстановку такого рода.

3.4 Поиск доказательства в системе резолюций

Резолюция представляет собой правило вывода, с помощью которого можно вывести новую ППФ (правильно построенную формулу) из старой. Однако в приведенном выше описании логической системы ничего не говорится о том, как выполнить доказательство. Обратим основное внимание на стратегические аспекты доказательства теорем.

Пусть р представляет утверждение "Сократ — это человек", a q — утверждение "Сократ смертен". Пусть наша теория имеет вид

Т={{¬р,q}, {р}}.

Таким образом, утверждается, что если Сократ человек, то Сократ смертен, и что Сократ — человек. {17} выводится из теории Т за один шаг резолюции, эквивалентной правилу modus ponens. .

Выражения {¬р, q} и {р} "сталкиваются" на паре дополняющих литералов р и ¬р, а {q} является резольвентой. Таким образом, теория Алогически подразумевает д, что записывается в форме Т|-q. Теперь можно добавить новую фразу {q} — резольвенту — в теорию Т и получить таким образом теорию

Т'= {{ ¬ip, q}, {p}, {q}}.

Конечно, в большинстве случаев для доказательства требуется множество шагов. Положим, например, что теория Т имеет вид

В этой теории р и q сохраняют прежний смысл, а г представляет утверждение "Сократ — бог". Для того чтобы показать, что Т|- ¬r , потребуются два шага резолюции:

{¬q,p},{Р}/{q}

{¬q,-r},{q} / {-r}

Обратите внимание, что на первом шаге используются две фразы из исходного множества Т, а на втором— резольвента {q}, добавленная к Т. Кроме того, следует отметить, что доказательство может быть выполнено и по-другому, например:

{¬p,q},{¬q,¬r}/{¬p,¬r},

{¬p,¬r},{p}/{¬r}

При таком способе доказательства к Т добавляется другая резольвента. В связи со сказанным возникает ряд проблем.

Когда множество Т велико, естественно предположить, что должно существовать несколько способов вывести интересующую нас конкретную формулу (эта формула является целевой). Естественно, что предпочтение следует отдать тому методу, который позволяет быстрее сформулировать доказа