Доказательства

Теперь нам известно все, что необходимо для создания формальных доказательств в контексте исчисления высказываний. Задача доказательства состоит в определении, будет ли некоторая данная формула д, т.е. заключение, логическим следствием (выводом) некоторого набора формул fl, f2,fn, т.е. предпосылок. Ниже дано символическое представление доказательства.

fl, f2, fn [ д

Такая форма записи с использованием символа метаутверждения р интерпретируется как gr следует из fl, f2, fn . Подобный способ выполнения называется прямым формированием цепочки и заключается в последовательном применении правил вывода к предпосылкам, затем - к формулам, выведенным из этих предпосылок, затем - к формулам, выведенным из этих формул, и т.д. до тех пор, пока не будет выведено заключение. Иначе говоря, процесс последовательного связывания состоит в переходе от предпосылок к заключению. Однако существует несколько вариантов этой основной схемы.

1. Принятие предпосылки. Если заключение д имеет вид р => д, то р принимается как дополнительная предпосылка, а q выводится из заданных предпосылок и предпосылки р.

2. Обратное формирование цепочки. Вместо доказательства утверждения р => g доказывается его контрапозиция (утверждение, обратное противоположному), т.е. NOT g => NOT p.

3. Приведение к противоречию. Вместо доказательства прямого утверждения р => g полагают, что р и NOT g являются истинными, и затем приходят к противоречию.

4. Резолюция. В этом методе вывода используется правило резолюции (п. 6 предыдущего перечня).

Методику использования правила резолюции следует рассмотреть подробнее, поскольку она широко применяется на практике и, в частности, обобщается для исчисления предикатов, в чем мы убедимся в разделе 23.4.

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

f OR gr NOT gr OR Л

В этом случае д и NOT д по правилу резолюции можно сократить до упрощенной формулы, f OR Л

В частности, на основе заданных формул f OR gr и NOT д (т.е. допуская, что h является истинным) можно вывести f.

Таким образом, можно отметить, что в общем случае данное правило применяется к конъюнкции (AND) двух формул, каждая из которых является дизъюнкцией (OR) двух формул. Для применения правила резолюции нужно поступить следующим образом. (Чтобы

обсуждение этого вопроса было более конкретным, рассмотрим его на примере.) Допустим, что необходимо определить, будет ли верным следующее предполагаемое доказательство (где А, В, Си Dявляются формулами).

Л => ( В => С ), NOT £> OR Л, В \- D С

Сначала следует принять отрицание заключения в качестве дополнительной предпосылки, а затем записать каждую предпосылку в отдельной строке.

Л => ( В => С ) NOT Z? OR Л В

NOT ( Z? => С )

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

Теперь нужно конвертировать каждую отдельную строку в конъюнктивную нормальную форму, т.е. в форму, состоящую из нескольких объединенных связками AND формул, каждая из которых может содержать связки NOT и OR, но не связку AND (подробнее это описано в главе 17). В рассматриваемом примере вторая и третья строки уже имеют требуемый вид. В двух других строках следует исключить все вхождения связки => , используя для этого ее определение на основе связок NOT и OR. В случае необходимости можно применить упомянутые выше дистрибутивные законы и законы Де Моргана. Кроме того, необходимо убрать лишние скобки и пары смежных связок NOT, которые образуют двойное отрицание. После выполнения всех этих действий строки примут следующий вид.

NOT Л OR NOT S OR С

NOT D OR Л

D AND NOT С

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

NOT Л OR NOT S OR С

NOT Z? OR Л

NOT С

Далее для объединения строк начнем применять правило резолюции. Для этого выберем пару совмещаемых строк, одна из которых содержит часть формулы, а другая - ее отрицание. Например, выберем первые две строки, содержащие NOT Л и Л соответственно. После их совмещения получится следующий результат.

NOT D OR NOT В OR С

NOT С

{Замечание. В общем случае необходимо также сохранить две исходные строки, однако в данной ситуации они больше не нужны.) Теперь можно снова применить правило резолюции для первых двух строк (совмещая NOT S и S), в результате чего будет получено следующее.

NOT D OR С D

NOT С

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

NOT С

Наконец после заключительного совмещения (С и NOT С) будет получено пустое множество заключений, которое обычно обозначается как [ ] и представляет собой противоречие. Таким образом, путем приведения к противоречию получен нужный результат.

23.4. Исчисление предикатов

Основным отличием исчисления предикатов от исчисления высказываний является использование в формулах исчисления предикатов переменных и кванторов. Благодаря этому эффективность и диапазон применения формул значительно увеличиваются. Например, утверждения Поставщик с номером S1 поставляет некоторую деталь с номером р и Некоторый поставщик с номером s поставляет некоторую деталь с номером р нельзя использовать в исчислении высказываний, однако это вполне допустимо в исчислении предикатов. Таким образом, в исчислении предикатов можно составлять запросы наподобие Какие детали поставляются поставщиком с номером S1? , Найти поставщиков, поставляющих некоторые детали и даже Найти поставщиков, которые вовсе не поставляют никаких деталей .

Предикаты

Как указывалось в главе 3, предикат - это логическая функция, которая при заданных для ее параметров аргументах возвращает значение истина или ложь. Например, выражение >(х,у) (оно чаще записывается в виде х>у) является предикатом с двумя параметрами, X и у. Этот предикат возвращает значение истина, если аргумент, соответствующий параметру х, больше аргумента, соответствующего параметру у, и значение ложь- в противном случае. Предикат, содержащий л аргументов (что равносильно предикату, содержащему л параметров), называется л-местным предикатом. Утверждение (т.е. формула в смысле, определенном в разделе 23.3) может рассматриваться как нуль-местный предикат, поскольку не имеет параметров и оценивается либо как истинное, либо как ложное утверждение.

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