Конъюнктивная нормальная форма для логики первого порядка
Как и в случае пропозициональной логики, для резолюции в логике первого порядка требуется, чтобы высказывания находились в конъюнктивной нормальной форме (Conjunctive Normal Form — CNF), т.е. представляли собой конъюнкцию выражений, в которой каждое выражение представляет собой дизъюнкцию литералов6. Литералы могут содержать переменные, на которые, согласно принятому предположению, распространяется квантор всеобщности. Например, высказывание
Vx American(х) л Weapon{y) л Sells{x,y,z) л Hostile{z) => Criminal{x)
принимает в форме CNF следующий вид:
-American (х) v —Weapon (у) v —tSells (х, у, z) v —iHostile{z) v Criminal (x)
Каждое высказывание в логике первого порядка может быть преобразовано в эквивалентное с точки зрения логического вывода высказывание CNF. В частности, высказывание CNF является невыполнимым тогда и только тогда, когда невыполнимо первоначальное высказывание, поэтому мы получаем основу для формирования доказательств от противного с помощью высказываний CNF.
Процедура преобразования любого высказывания в форму CNF весьма подобна процедуре, применяемой в пропозициональной логике, которая показана на с. 308. Принципиальное различие связано с необходимостью устранения кванторов существования. Проиллюстрируем эту процедуру на примере преобразования в форму CNF высказывания "Каждого, кто любит всех животных, кто-то любит", или
Vx [Vy Animal (у) => Loves (х, у) ] => [Зу Loves (у, х) ]
Ниже приведены этапы этого преобразования.
• Устранение импликаций:
Vx [-iVy -nAnimal (у) v Loves {х, у) ] v [Зу Loves (у, х) ]
• Перемещение связок -i внутрь выражений. Кроме обычных правил для отрицаемых связок, нам нужны правила для отрицаемых кванторов. Поэтому получаем следующие правила:
—iVx p принимает вид Зх —ip -i3x p принимает вид Vx -p
Рассматриваемое высказывание проходит через такие преобразования:
Vx [Зу -1 (-Animal (у) v Loves (х, у))] v [Зу Loves (у, х)] Vx [Зу -r-iAnimal (у) л -iLoves (х, у) ] v [Зу Loves (у, х) ] Vx [Зу Animal (у) л —lLoves (х, у) ] v [Зу Loves (у, х) ]
Обратите внимание на то, что квантор всеобщности (Vy) в предпосылке импликации стал квантором существования. Теперь это высказывание приобрело такое прочтение: "Либо существует какое-то животное, которого х не любит, либо (если это утверждение не является истинным) кто-то любит х". Очевидно, что смысл первоначального высказывания был сохранен.
• Стандартизация переменных. В высказываниях наподобие (Vx Р{х) ) v (Зх Q(x) ), в которых дважды используется одно и то же имя переменной, изменим имя одной из переменных. Это позволит в дальнейшем избежать путаницы после того, как будут удалены кванторы. Поэтому получим следующее:
Vx [Зу Animal (у) л -nLoves (х,у) ] v [3z Loves (z,x) ]
• Сколемизация. Сколемизация — это процесс устранения кванторов существования путем их удаления. В данном простом случае этот процесс подобен применению правила конкретизации с помощью квантора существования, приведенного в разделе 9.1: преобразовать Зх Р(х) в Р(А), где А — новая константа. Однако, если это правило будет непосредственно применено к высказыванию, рассматриваемому в качестве примера, то будет получено следующее высказывание:
Vx [Animal (А) л -\Loves (х, А) ] v Loves (В, х)
которое имеет полностью неправильный смысл: в нем утверждается, что каждый либо не способен любить какое-то конкретное животное А, либо его любит некоторая конкретная сущность В. В действительности первоначальное высказывание позволяет каждому человеку не быть способным любить какое-то другое животное или быть любимым другим человеком. Поэтому желательно, чтобы сущности, определяемые в процессе сколемизации, зависели от х:
Vx [Animal (F(x) ) л —iLoves (х, F(x) ) ] v Loves (G(x) , x)
где F и G— сколемовские функции. Общее правило состоит в том, что все параметры сколемовской функции должны быть переменными, на которые распространяются кванторы всеобщности, в область действия которых попадает соответствующий квантор существования. Как и при использовании конкретизации с помощью квантора существования, сколемизированное высказывание является выполнимым тогда и только тогда, когда выполнимо первоначальное высказывание.
• Удаление кванторов всеобщности. В данный момент на все оставшиеся переменные должны распространяться кванторы всеобщности. Кроме того, данное высказывание эквивалентно тому, в котором все кванторы всеобщности перенесены влево. Поэтому кванторы всеобщности могут быть удалены следующим образом:
[Animal (F(x) ) л -iLoves (x, F(x) ) ] v Loves (G{x) , x) • Распределение связки v по л:
[Animal (F(x) ) v Loves (G (x) , x) ] л [-iLoves (x, F(x) ) v Loves (G (x) , x) ]
На этом этапе может также потребоваться выполнить раскрытие скобок во вложенных конъюнкциях и дизъюнкциях.
Теперь рассматриваемое высказывание находится в форме CNF и состоит из двух выражений. Оно полностью недоступно для восприятия. (Помочь его понять может такое пояснение, что сколемовская функция F(x) указывает на животное, которое потенциально может быть нелюбимым лицом х, a G{x) указывает на кого-то, кто может любить лицо х.) К счастью, людям редко приходится изучать высказывания в форме CNF, поскольку показанный выше процесс преобразования может быть легко автоматизирован.