На этом шаге мы рассмотрим хорновские дизънкты.
Дизъюнкт - это совокупность литер, одни из которых не содержат, а другие содержат
знак отрицания. Если первые записывать через точку с запятой слева от знака ":-", а вторые
- без знака отрицания через запятую справа от знака ":-" и в конце каждого дизъюнкта ставить точку,
то получим выражение вида:
A1;A2;…;An:-
B1,B2,…,Bm
Из каждых двух дизъюнктов, представленных в таком виде, используя метод резолюций, можно
получить новый дизъюнкт, являющийся следствием двух первых. Если одна и та же атомарная
формула появляется в левой части одного дизъюнкта (литера без отрицания) и в правой части другого
(литера с отрицанием), то новый дизъюнкт, полученный в результате слияния исходных дизъюнктов и
вычеркивания повторяющейся рассматриваемой атомарной формулы, является следствием исходных дизъюнктов.
При форме записи это означает вычеркивание контрарных пар, находящихся по разные стороны от знака ":-".
Например, даны два дизъюнкта:
A;B;C:-D,E,F.
G;H:-A,M,N.
Полученный в результате их слияния и вычеркивания повторяются литеры A новый дизъюнкт:
B;C;G;H:-D,E,F,M,N
является следствием исходных. Вычеркивание повторяющейся слева и справа от знака ":-"
литеры А аналогично рассмотренномy ранее вычеркиванию контрарной пары А и ~А.
Метод резолюций допускает сопоставление нескольких литер в левой части одного дизъюнкта с несколькими литерами в правой части другого.
Если дизъюнкты содержат переменные, то для получения резольвенты атомарные формулы не обязательно должны быть идентичными, они должны быть лишь сопоставимыми (унифицируемыми). При сопоставлении формул происходит конкретизация значений переменных (конкретизация переменных), в результате которой формулы становятся идентичными. Например, при сопоставлении формул A(x) и A(b) происходит конкретизация переменной x, которая принимает значение, равное b.
Хорновский дизъюнкт - это дизъюнкт, содержащий не более одной литеры без отрицания. Например:
A:-B,C,D;
A:-B1,B2,Bn.
Приведенным хорновским дизъюнктам эквивалентны следующие формулы логики предикатов первого порядка:
BÙCÙD
®A;
B1ÙB2Ù
Bn
®A
(переменные в этих формулах не указаны).
Существует два вида хорновских дизъюнктов.
Хорновский дизъюнкт с заголовком - это дизъюнкт, содержащий одну литеру без отрицания.
Он может содержать одну или несколько литер с отрицанием или не содержать их вообще, например:
A:-B,C, ...,D;
A:-B;
A:-.
Последний из приведенных дизъюнктов можно записывать без знака ":-", то есть в виде А.
Хорновский дизъюнкт без заголовка - это дизъюнкт, не содержащий литер без отрицания, например:
:-B,C, ...,D;
:- A.
В результате применения метода резолюций к двум хорновским дизъюнктам с заголовками вновь получается хорновский дизъюнкт с заголовком. Известно, что пустой дизъюнкт не имеет заголовка. Следовательно, если все дизъюнкты имеют заголовки, то из них могут быть получены только дизъюнкты с заголовками.
Таким образом, для того чтобы из исходных дизъюнктов, отрицая доказываемое высказывание, можно было бы вывести пустой дизъюнкт, необходимо наличие, по крайней мере, одного дизъюнкта без заголовка.
Если среди исходных имеется несколько дизъюнктов без заголовка, то доказательство каждого нового дизъюнкта методом резолюций может быть преобразовано в доказательство, в котором используется не более чем один дизъюнкт без заголовка. Если пустой дизъюнкт следует из заданного множества исходных, то он следует и из его подмножества, содержащего дизъюнкты с заголовками и не более одного дизъюнкта без заголовка.
Любая задача, которая может быть выражена с помощью хорновских дизъюнктов, должна иметь только один дизъюнкт без заголовка (целевой); все остальные дизъюнкты должны быть с заголовками (гипотезы).
Хорновские дизъюнкты были выбраны в качестве основы для создания программных систем автоматического доказательства теорем.
Метод резолюций для хорновских дизъюнктов более прост. Поэтому в Прологе используется ограниченный вариант метода резолюций, рассчитанный на работу с одной литерой в левой части.
Со следующего шага мы начнем рассматривать основы языка Пролог.
