Cтраница 1
Метод аналитических таблиц в общем случае не является детерминированным, поэтому Фиттингом предложена очередность применения правил. [1]
Метод аналитических таблиц ( или метод семантических таблиц, или метод Хинтикка) является эффективной процедурой доказательства теорем, как для логики высказываний, так и для логики предикатов первого порядка. Но если метод резолюции работает с формулами, представленными в КНФ, то метод аналитических таблиц оперирует с формулами, представленными в ДНФ. Вывод осуществляется на бинарных деревьях, вершины которых отмечены формулами, причем вершина называется концевой, если она не имеет потомков, простой, если она имеет только одного потомка и дизъюнктивной, если она имеет двух потомков. Каждая ветвь дерева представлена конъюнкцией формул, а само дерево - дизъюнкцией своих ветвей. [2]
Поскольку метод аналитических таблиц основан на процедуре опровержения, то для доказательства общезначимости формулы X надо построить дерево ( таблицу) для ЛХ ( - Х), которое будет замкнутым. [3]
Докажем методом аналитических таблиц пример, который был до этого доказан с помощью принципа резолюции. [4]
Полное описание метода аналитических таблиц дано в книге [4.1], из которой был почерпнут основной материал для написания этой главы. [5]
Перед описанием реализации метода аналитических таблиц для логики 1-го порядка приведем основные теоретические положения, лежащие в его основе. [6]
В главе 4 описан метод аналитических таблиц, который малоизвестен русскоязычному читателю вследствие малого количества литературы по этому методу на русском языке. [7]
Отсюда очевидна теорема о состоятельности метода аналитических таблиц для логики предикатов первого порядка. [8]
Теперь нам осталось показать, что метод аналитических таблиц обладает непротиворечивостью и полнотой. [9]
X общезначима, то она доказуема методом аналитических таблиц. Однако сначала покажем, что если имеется открытая ( незамкнутая) ветвь на дереве, то таблица будет выполнимой. [10]
Поскольку вслед за Фиттингом нами приведено несколько реализаций метода аналитических таблиц, зададимся вопросом: какая из реализаций является лучшей. [11]
Если формула X общезначима, то она доказуема методом аналитических таблиц. [12]
Теорема 4.1. Если формула X выводима ( доказуема) методом аналитических таблиц, то она общезначима. [13]
Теорема 4.6. Если формула X логики предикатов первого порядка доказуема методом аналитических таблиц, то она общезначима. [14]
Следует отметить еще одну деталь, приводящую к неэффективности заключительной версии метода аналитических таблиц. Предположим, что аналитическая таблица построена до момента, начиная с которого она разветвляется на 5 ветвей, 4 из которых являются замкнутыми. Предикат, названный expand and close, будет тестировать на замкнутость все ветви таблицы и найдет ветвь, которая не является замкнутой. Затем применяется правило расширения таблицы, и снова вся таблица тестируется на замкнутость ветвей. [15]