- •Логика высказываний
- •1. Введение в логику высказываний. Логические связки
- •2. Особенности построения доказательств в логике высказываний
- •3. Аксиоматический метод доказательства логических клауз
- •4. Конструктивный метод доказательства логических клауз
- •5, Доказательство логических клауз принципом резолюций
- •6. Доказательство логических клауз методом Вонга
- •7. Доказательство логических клауз методом натурального исчисления
5, Доказательство логических клауз принципом резолюций
Принцип резолюций играет роль аксиомы порядка и вместе с тем порождает очень эффективную конструктивную процедуру. Суть его сводиться к тому, что два посылочных дизъюнкта с противоположными термами всегда можно склеить в один заключительный дизъюнкт, в котором уже не будет противоположных термов:
где X и Y - произвольные термы или целые дизъюнкты с любим набором термов, включая ноль, А и - произвольные термы.
При последовательном применении принципа резолюций происходит уменьшение числа букв, вплоть до их полного исчезновения. При этом исходная клауза конструируется в форме конъюнктивного противоречия:
Докажем с помощью метода резолюций справедливость правила отделения:
или
Здесь имеются три дизъюнкта Склеивая их последовательно, получаем в результате ноль, который говорит о несовместимости заключения и посылок. Это как раз и свидетельствует о справедливости исходной клаузы.
Принцип резолюций целиком заменяет аксиому порядка, поскольку сама эта аксиома может быть доказана в рамках метода резолюций. Действительно,
Обратим внимание, что посылка В здесь вообще не используется. Необходимо иметь в виду, что все посылки (их число часто бывает избыточным) использовать необязательно - главное получить ноль. Пусть дана клауза
Доказательство ее справедливости следует начать с приведения ее в НКФ:
Выпишем по порядку все посылки и далее начнем их склеивать согласно очередности. Справа от каждого дизъюнкта будем писать номера используемых дизъюнктов, получим:
( 1,3 )
( 1,4 )
( 2,3 )
( 2,4 )
( 2,5 )
( 3,6 )
( 3,8 )
( 4,5 )
( 4,7 )
0. ( 4,9 )
Подобная стратегия поиска нуля непродуктивна. Если к этой задаче подойти более творчески, то ноль обнаружится на четвертом шаге от начала поиска: 5. В ( 1,4 ), 6. С ( 2,4 ), 7. ( 3,6 ), 8. 0 ( 5,7 ).
До сих пор речь шла о форме конъюнктивного противоречия. Исходя из принципа двойственности, метод резолюций можно сформулировать относительно дизъюнктивной тавтологии, при этом принцип резолюций изменится:
Докажем одну и ту же клаузу двумя способами - в форме противоречия и в форме тавтологии. Пусть дана клауза:
Доказательство в форме противоречия выглядит следующим образом:
Склейки: 5. B ( 1, 2 ), 6. ( 1, 6 ), 7. С ( 3, 5 ), 7. 0 ( 4, 7 ).
Доказательство в форме тавтологии выглядит аналогично:
Склейки: 5. ( 1, 2 ), 6. ( 2, 3 ), 7. ( 1, 6 ), 7. 1 ( 4, 7 ).
Метод резолюций легко поддается алгоритмизации. Алгоритм склеек образует структуру древовидной формы, что хорошо видно для следующей клаузы (рис. 10.1.):
Рис. 10.1. Структура древовидной формы.
6. Доказательство логических клауз методом Вонга
В методе Вонга используется сконструированная конъюнктивно-дизъюнктивная нормальная форма представления исходной клаузы, а аксиому порядка заменяет клауза Вонга:
где X пробегает некоторые буквы, входящие в клаузу, a L и К - определенные комбинации дизъюнктов и конъюнктов.
Конструктивная процедура доказательства сводится к последовательному разбиению дизъюнктов или конъюнктов таким образом, чтобы слева и справа от метаимпликапда появлялась одна и те же буква X. Если в результате такого разбиения все конечные клаузы приобретают вид клаузы Вонга, то и исходная клауза была составлена верно. Разберем метод Вонга на примере доказательства справедливости правила отделения:
или .
Здесь имеется только один дизъюнкт, который можно подвергнуть разбиению. После его разбиения получим две новые клаузы:
и
Вторая клауза удовлетворяет и аксиоме порядка и клаузе Вонга. В качестве X в ней выступает B, L = A и R = 0. Первая же клауза тоже будет удовлетворять необходимым требованиям, но только после того, как терм из левой части клаузы с противоположным знаком перенести в правую часть. Получаем:
где X = A, L = 1, R = B
При большом числе букв в исходной клаузе прибегают к специальной нумерации произвольных клауз, чтобы не запутаться. Пусть требуется установить справедливость cледующей клаузы:
Приведем ее в соответствующую конъюнктивно-дизъюнктивную нормальную форму:
Далее произведем разбиение первого дизъюнкта, в результате получим две произвольные клаузы:
Клауза (1) отбрасывается, так как она удовлетворяет клаузе Вонга. Разбивая следующий дизъюнкт клаузы (2), получаем еще три новых клаузы:
2.1.
2.2.
2.3.
Клаузы ( 2.1. ) и ( 2.2. ) сводят к одной клаузе
2.1.
Произведём её разбиение:
2.1.1.
2.1.2.
2.1.3
Первые две клаузы удовлетворяют клаузе Вонга. У клаузы ( 2.1.3. ) нужно разбивать конъюнкт:
2.1.3.1.
2.1.3.2
Теперь обе клаузы имеют вид Вонга. Но у нас еще осталась ветвь ( 2.3. ), она отличается от рассмотренной ветви ( 2.1. ) наличием непарного терма U, который, однако, не может повлиять на конечный результат, то есть разбиение клаузы ( 2.3.) практически полностью совпадает с разбиением клаузы ( 2.1.). Следовательно, исходная клауза была записана верно.