Теоремы матлогики
Лекция 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 этих дизъюнкт заменяет
в множестве
.
Продолжают процесс до вывода пустого или до невозможности такого дизъюнктивного вывода. Такой вывод невозможен, если множество не содержит пары дизъюнктов описанного типа.
Пример:
№ |
|
Дизъюнкты |
||||
D1 |
D2 |
D3 |
D4 |
D5 |
||
1 2 3 |
S0 S1 S2 |
|
|
T* T T |
A A* A |
|
Пустой дизъюнкт не выведен. Исходное множество дизъюнктов не противоречиво.
Имеется теорема о корректности метода.
Теорема.
Исходное множество хорновских дизъюнктов противоречиво существует хорновский вывод пустого дизъюнкта (
.
Лекция 6.