Теоремы матлогики

Лекция 5.

Закон резолюции:

1.  , следовательно

2.  Если ч. т.д.

Противоречивость (не выполнимость) множества дизъюнктов:

множество называется противоречивым, если формула есть противоречие:

Для выражения противоречия применяется метод резолюции. Это один из возможных методов. В логике высказываний это можно решить и по-другому.

Метод резолюций в логике высказываний.

Метод систематического вычисления двоичных резольвент некоторого расширяющегося множества дизъюнктов, содержащего множества дизъюнктов. Основа – закон резолюций.

1.  Метод насыщения уровня (метод полного перебора).

1)  Составляем S0 (исходное множество дизъюнктов)

2)  Пусть уже построены множества

тогда для построения Sn необходимо к имеющемуся списку дизъюнктов приписать двоичные резольвенты дизъюнктов , так что i<j

,

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

4)  Если пустой дизъюнкт выводится, то исходное множество дизъюнктов противоречиво .

Пример:

: 1)

2)

3)

4)

: 5) (1-2)

6) (1-3)

7) (1-4)

8) (2-4)

9) ???(2-3)

10) (2-4)

11) (3-4)

: 12) (1-7)

13) (1-8)

14) (1-9)

…

n-2) (5-7)

n-1) (5-9)

n)

2.  Стратегия вычеркивания.

Устраняет недостатки предыдущего метода:

– повторяющиеся резольвенты

– тавтологии

– наддизъюнкты существующих

Пример:

: 1)

2)

3)

4)

: 5) (1-2)

6) (1-3)

7) (1-4)

8) (2-4)

9) ???(2-3)

10) (2-4)

11) (3-4)

: 12) (1-7)

13) (1-8)

14) (1-9)

…

n-2) (5-7)

n-1) (5-9)

n)

3.  Лок-резолюции.

Все литералы исходного множества дизъюнктов номеруются. И при вычислении двоичной резольвенты рассматриваются лишь литералы, имеющие наименьшие номера в каждом из дизъюнктов, т. е. число рассматриваемых пар литералов уменьшается.

Пример:

: 1)

2)

3)

4)

! Нумерация наследуют свои индексы. Если литерал наследует несколько индексов, то оставляется наименьший.

: 5) (1-2)

6) (1-4)

7) (2-3)

8) (3-4)

…

(5-8)

Другая нумерация:

: 1)

2)

3)

4)

S1: 5) (1-2)

S2: 6) (3-5)

7) (4-5)

Доказано, что результат работы этого алгоритма не зависит от нумерации литералов исходного множества дизъюнктов.

Доказано, что этот метод коректин, т. е. множетсво дизъюнктов противоречив тогда и только тогда, когда существует лок–вывод пустого дизъюнкта.

4.  Метод резолюций для хорновских дизъюнктов.

Метод применим только в частных случаях, когда дизъюнкты хоновские.

– называется позитивным литералом.

– называется негативным литералом.

Дизъюнкт называется хорновским, если он содержит не более одного позитивного литерала.

– называется точным литералом.

– называется негативным литералом.

– называется унарно позитивным.

– называется унарно негативным.

Если все дизъюнкты хорновские, то процесс вывода резолюции сильно упрощается.

1.

2.

содержит все резольвенты дизъюнкции

– называется унарно позитивным дизъюнктом.

,

(, который содержит L контрарный )

В множестве резольвента R этих дизъюнкт заменяет в множестве .

Продолжают процесс до вывода пустого или до невозможности такого дизъюнктивного вывода. Такой вывод невозможен, если множество не содержит пары дизъюнктов описанного типа.

Пример:

Пустой дизъюнкт не выведен. Исходное множество дизъюнктов не противоречиво.

Имеется теорема о корректности метода.

Теорема.

Исходное множество хорновских дизъюнктов противоречиво существует хорновский вывод пустого дизъюнкта (.

Лекция 6.