Принцип резолюции

В ЛП все решаемые задачи могут быть представлены в виде теорем, которые должны быть доказаны в рамках исчисления предикатов первого порядка. Робинсон предложил удачный метод работы с предложениями. Этот метод легко реализуется на ЭВМ. В основе предложения Робинсона лежит принцип резолюции и основанные на нем методы доказательства теорем. Принцип резолюции – это метод вывода, который является непротиворечивым и полным. Это значит, что этим методом можно доказать лишь справедливые теоремы, причем если теорема справедлива, то она доказывается за конечное число шагов. Мы считаем множество S (наши утверждения) – внутренне непротиворечивыми. Непротиворечивость множества S будет гарантирована всякий раз, когда это множество содержит только правила и/или факты – а именно так обстоит дело в стандартном логическом программировании.

Основная стратегия доказательства заключается в том, чтобы показать несправедливость (противоречие) противоположной теоремы, а не пытаться непосредственно вывести исходную теорему (доказательство от противного - reductio absurdum)

У нас есть программа:

S1={F ,…..,F_n} – множество формул в разделе утверждений (clauses).

F - цель (goal)

Формула F логически следует из S1,если при каждой интерпретации, когда все F -истинны (то есть истинна их конъюнкция) истинной является и F . Иначе, каждая интерпретация, удовлетворяющая S1, удовлетворяет и F .

С точки зрения Пролога это означает, что формула, которую нужно доказать в прикладном исчислении предикатов первого порядка, должна логически следовать из множества формул, составляющих программу. Иначе программа будет работать неправильно, или приведет к неправильному результату.

Для того чтобы доказать, что F_n+1 логически следует из S1, можно доказать, что множество

S2=S1 { F } является противоречивым, то есть

не существует интерпретации, в которой оно бы удовлетворялось.

В логике есть два классических правила вывода, открытых очень давно. Это – модус поненс и цепное заключение.

1.Modus Ponens -правило сокращения посылки путем применения импликации (отношение если….то) Если истинно А и истинно А--à(влечет)В, то можно вывести В(но не наоборот). То есть из двух данныхпредложений можно вывести третье(B).Корректность правила очевидна. Она получается из определения операции ВЛЕЧЕТ. Правило применимо к любой формуле.

(A

A-àB

B)

(“А влечет В” или “если А,то В”) Рассуждения уместны только в одном направлении: зная А можно получить В, но не наоборот).Утверждение “если А, то В” будет правильным независимо от того, истинно В или ложно.

2.Цепное правило –позволяет вывести новую импликацию из двух данных импликаций.

Если истинно А-àВ и истинно В-àС, то можно вывести А-àС.Корректность очевидна: если истинность А влечет истинность В, и истинность В влечет истинность С, то истинность А влечет истинность С.

Из А àВ

В àС

Получаем АàС

Проблема доказательства в логике состоит в нахождении доказательства заключения на основании посылок.

Это можно сделать либо табличным способом с помощью построения таблиц истинности (алгебра логики), либо с помощью применения правил вывода.

Метод резолюции в исчислении предикатов – это пра -

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

Метод резолюции является более общим по отношению к модус поненс и цепному правилу. Модус поненс является частным случаем правила резолюции для случая ложного А. Правило резолюции можно рассматривать как аналог цепного правила в применении к формулам, находящимся в конъюнктивной нормальной форме. (Любое выражение в ИП1П можно привести к КНФ - по сути похоже на упрощение алгебраических выражений).

Резолюция – это метод доказательства того, что ложное высказывание – ложно, а не того, что истинное высказывание - истинно. Необходимо понимать, что такое логическое следствие и логический вывод.

Предложения программы сами по себе не являются true или false.Значения true или false для предложения определяются их конкретной интерпретацией. Решая задачу мы всегда выбираем определенную область интерпретации (предметную область), которая представляет собой произвольное множество объектов (D).{На основе теоретико-множественной модели}. Эти объекты сопоставляются именам, входящим в наши предложения (S1).

Наши предложения (S1) Область интерпретации(D)

сonst -------------------------------объект

функтор -------------------------------функция

предикат -------------------------------отношение

{true,false}

Используем интерпретацию множества предложений S1 для оценки каждого предложения из S1 с помощью истинностных значений true и false.

Каждое предложение из S1 будет принимать в данной интерпретации true или false. Сказать, что некоторое предложение из S1 истинно или ложно относительно выбранной интерпретации, значит сказать, что истинно или ложно соответствующее высказывание о D.

Таким образом, посредством установления связи с внешним миром объектов предложения S1 приобретают истинностно - функциональное значение.