Синтаксический способ

Рассмотрим данную задачу как теорию предметной области, которой соответствует набор аксиом и в которой верны правила вывода. В качестве аксиом теории выберем утверждения, высказанные задержанными:

1. Б Ù ù Д;

2. ù Б Ù С;

3. Б Ù ù С.

По условиям задачи только одно утверждение является истинным (“правду говорил старик”) и, следовательно, только один из вариантов утверждений является аксиомой теории. Рассмотрим предположение, что первое утверждение является аксиомой, тогда третье утверждение тоже правда, т.к. преступник был один, если предположить, что третье утверждение – аксиома, то по этой же причине первое утверждение тоже правда, а это противоречит условиям задачи (“правду говорил только один”). Следовательно, единственно верной аксиомой этой теории является второе утверждение, которое высказал Джон, о том, что Браун не виноват, а преступление совершил Смит. Таким образом, получаем следующее решение задачи: Джон-старик, Смит-преступник, Браун-чиновник. В данном примере синтаксический способ решения задачи кажется более простым и лёгким, таким образом, как уже отмечалось выше, трудоёмкость способа определяется задачей.

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

Синтаксический способ для исчисления предикатов.

Пример: Доказать, что формула $ x (R (x) Ù (B ® T(x)))® ®(" x (R(x)® ù T(x))®ù B) является общезначимой.

Используя равносильности алгебры высказываний и алгебры

предикатов проведём следующие преобразования этой формулы:

$ x (R (x) Ù (B®T(x)))®(" x (R(x)®ù T(x))®ù B) º $ x (R (x) Ù Ù (ù B Ú T(x)))® (ù " x (R(x)®ù T(x)) Úù B) º $ x ((R (x) Ù T(x)) Ú Ú (R (x) Ù ù B))®($ xù (ù R(x) Úù T(x)) Úù B) º ($ x (R (x) Ù T(x)) Ú Ú ($ x R (x) Ù ù B))®($ x (R(x) ÙT(x)) Úù B) ºù ($ x (R (x) Ù T(x)) Ú Ú ($ x R (x) Ù ù B)) Ú ($ x (R(x) ÙT(x)) Úù B) º (ù $ x (R (x) ÙT(x)) Ù Ùù ($ x R (x) Ùù B)) Ú ($ x (R(x) ÙT(x)) Úù B) º (ù $ x (R (x) ÙT(x)) Ù Ù (ù $ x R (x) Ú B)) Ú ($ x (R(x) ÙT(x)) Úù B) º (ù $ x (R (x) ÙT(x)) Ú Ú $ x (R(x) ÙT(x)) Úù B) Ù (ù $ x R (x) Ú B Ú $ x (R(x) ÙT(x)) Úù B) º

º истина Ù истина º истина. Исходная формула общезначима.

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

В связи с этим возникает задача построения формальной процедуры (алгоритма) определения к какому классу относится данная формула? Эта задача носит название проблемы разрешимости. Очевидно, проблема разрешимости алгебры высказываний разрешима, т.к. для каждой формулы алгебры логики может быть формально построена таблица истинности, которая и даст ответ на поставленный вопрос. Проблема разрешимости в алгебре предикатов ставится также, как в алгебре высказываний: существуют ли алгоритмы, позволяющие для любой формулы A алгебры предикатов установить к какому классу она относится, то есть, является ли общезначимой, или выполнимой, или тождественно-ложной. Отметим, что в отличие от алгебры высказываний здесь не применим метод перебора всех вариантов значений переменных, входящих в формулу, так как таких вариантов может быть бесконечное множество.

В 1936г. американский математик А.Черч доказал, что проблема разрешимости алгебры предикатов в общем виде алгоритмически не разрешима, то есть не существует алгоритма, который бы позволил установить к какому классу формул относится любая формула алгебры предикатов. В этом смысле говорят о неразрешимости исчисления предикатов. Вместе с тем доказано (Эрбран, 1930г.), что исчисление предикатов первого порядка полуразрешимо, т.е. доказано существование процедуры подтверждения выводимости некоторой ППФ T из заданного множества формул B1,¼Bn, если известно, что эта ППФ является теоремой. Основной процедурой, позволяющей реализовать эту полуразрешимость, является правило резолюции Дж. Робинсона (1965 г.), имеющее различные модификации.

Теории первого порядка отличаются от теорий высших порядков тем, что не допускают в своём изложении предикаты, которые имеют в качестве возможных значений своих аргументов другие предикаты и функции. Кроме того, они не допускают кванторные операции по предикатам или функциям. Процесс доказательства теоремы некоторой теории или общезначимости ППФ для данной ситемы аксиом с использованием правила резолюций основан на опровержении отрицания этой ППФ. В этом случае к системе аксиом теории добавляется отрицание доказуемой ППФ и с помощью правила резолюций доказывается противоречивость новой системы аксиом. Такая схема построения доказательства теоремы называется процедурой опровержения. Ещё одним ограничением правила резолюций является то, что этот метод применим к аксиомам теории и доказуемой теореме только тогда, когда выражающие их формулы записаны в виде дизъюнкт (фраз, предложений) Хорна. Дизъюнкта Хорна это формула, состоящая из дизъюнкций одной позитивной и остальных негативных элементарных формул, т.е формула вида: ù A1 Ú ù A2Ú,¼,Ú ù An Ú B. Аксиомы теории, выраженные в виде дизъюнкт Хорна имеют вполне объяснимую интерпретацию.

Преобразуем общую форму дизъюнкта Хорна на основании закона равносильности к виду A1 Ù A2 Ù,¼, Ù An ®B, получим импликацию, в виде которой обычно записывают закон предметной области. Здесь из истинности посылок и самой импликации (формула является аксиомой теории) следует истинность заключения (обратное неверно: из ложности посылок не следует ложность заключения). Набор законов или система аксиом теории образуется путём объединения знаком конъюнкция (Ù) отдельных законов или аксиом теории. Однако, можно показать, что любую ППФ исчисления предикатов можно по определённой методике привести к дизъюнктам Хорна, объединённых знаком конъюнкции.

Дата добавления: 2015-06-27