На этом шаге мы рассмотрим этапы приведения формулы к стандартной форме записи.
В логике предикатов первого порядка процесс приведения формул к стандартной форме записи включает в себя семь этапов.
Например, формула ("x)(A(x))Ù ($x)B(x) в результате разделения переменных, то есть замены переменной x после попадания ее под действие квантора существования $ на переменную y, преобразуется к виду ("x)(A(x)) Ù($y)B(y).
Например, формула ($x)A(x) может быть заменена формулой A(b) при x=b, где b - константа.
Если формула содержит квантор общности, то надо вводить не константы, а составные термы (функциональные символы с множеством переменных аргументов), чтобы показать зависимость объекта от переменных.
Например, если в формуле:
("x)(Человек(x) - ($y)
Мать(x,y)),
обозначающей, что каждый человек имеет мать, удалить квантор существования $
y и поставить y=Мария, то получим, что все люди имеют одну и ту же мать по имени Мария, а это неверно. Здесь при
удалении квантора существования $ надо вводить не константу,
а составной терм, то есть функциональный
символ f(x), который каждому конкретному человеку ставит в соответствие его мать:
("x)(Человек(x)®
Мать(x,f(x))).
Формула в предваренной нормальной форме состоит из цепочки кванторов и следующей за ней бескванторной формулы. Так как область действия каждого квантора включает всю формулу, то кванторы сами по себе не несут больше какой-либо дополнительной информации и, следовательно, их можно опустить.
Так, после удаления кванторов всеобщности рассмотренная выше формула будет иметь следующий вид:
Человек(x)®Мать(x,f (x)).
Следовательно, каждая формула исчисления предикатов эквивалентна совокупности дизъюнктов, состоящих
из литералов и соединенных символами дизъюнкции. Слово "совокупность" подчеркивает, что порядок
дизъюнктов не имеет значения. Например, формулу:
A(x)ÙB(x)ÙC(x)
можно представить в виде совокупности дизъюнктов (знак дизъюнкции опущен):
{A(x), B(x), C(x)}.
Таким образом, любая исходная формула может быть записана в стандартной форме, то есть в виде совокупности дизъюнктов. Стандартная форма записи формул достаточно лаконична и выразительна, так как в ней опущены символы логических связок дизъюнкции и конъюнкции, а также кванторы всеобщности и существования.
Преобразование формулы к стандартному виду может быть выполнено вне зависимости от того, существует или нет интерпретация, при которой формула истинна.
Метод резолюций является полным. Если некоторый факт следует из исходных гипотез, то всегда можно доказать его истинность методом резолюций.
При рассмотрении логики высказываний было показано, что формула A является логическим следствием формул B1, B2, ..., Bn тогда и только тогда, когда формула B1ÚB2Ú… ÚBnÚ ~A противоречива, то есть доказательство того, что отдельная формула есть логическое следствие конечного множества формул, эквивалентно доказательству того, что некоторая связанная с ними формула общезначима или противоречива.
Так же и в логике предикатов, если множество формул {B1, B2,…, Bn} непротиворечиво, то формула А является следствием формул {B1, B2, ..., Bn} тогда и только тогда, когда множество формул {B1, B2,…, Bn, ~А} противоречиво.
Если множество исходных гипотез непротиворечиво, то надо добавить к нему дизъюнкты, отрицающие высказывание, которое следует доказать. Если доказываемое высказывание следует из заданных гипотез, то получим пустой дизъюнкт. Добавляемые к множеству гипотез дизъюнкты называются целевыми.
При доказательстве по методу резолюций возможно образование большого количества лишних дизъюнктов. Многие из таких дизъюнктов представляют собой общезначимые формулы, которые истинны при всех интерпретациях и не влияют на процедуру доказательств, а следовательно, их можно вычеркнуть.
Используя метод резолюций, можно автоматически доказывать теоремы, выводя их из аксиом. Необходимо лишь задать исходные высказывания, а следствие из них будет получено автоматически с помощью правил вывода.
На следующем шаге мы рассмотрим хорновские дизъюнкты.