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

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

S├ G.

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

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

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

Это означает, что теорема доказана, то есть S├ G.

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

Таким образом, исчисление предикатов является полуразрешимой теорией, а метод резолюций яв­ляется частичным алгоритмом автоматического доказательства теорем.

Например,докажем методом резолюций теорему ├;_L (((A В) А) А). Сначала нужно преобразовать в предложения отрицание целевой формулы ┐(((A В) А) А).

1. ┐(┐(┐(┐A B) A) A).

2. (((A&┐B) A)& ┐A).

3-6. Формула без изменений.

7. (A A)&(┐B A) &┐ A.

8. A A, ┐B A, ┐ A.

После этого проводится резольвирование имеющихся предложений 1-3.

1. A A.

2. ┐B A.

3. ┐ A.

4. А из 1 и 3 по правилу резолюции.

5. из 3 и 4 по правилу резолюции.

Таким образом, теорема доказана.

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