Cтраница 2
Теперь рассмотрим, каким образом лемма Хинтикка может быть использована для доказательства состоятельности и полноты метода аналитических таблиц для случая логики предикатов первого порядка. Прежде всего, рассмотрим лемму Кенига. [16]
Поскольку правило атомарного замыкания с помощью НОУ есть как раз специальный случай правила подстановки таблицы, его добавление в систему не будет влиять на свойство состоятельности метода аналитических таблиц. И можно доказать, что система полна, даже когда все применения правила подстановки таблицы ограничены применениями правила атомарного замыкания с помощью НОУ. [17]
Для того, чтобы читатель смог получить цельное представление о рассматриваемых проблемах, в книге, наряду с оригинальными работами авторов, составляющих единую научную группу, изложен ряд результатов других российских и зарубежных ученых, тем более, что некоторые проблемы и методы такие, как метод аналитических таблиц или проблема аргументации и абдукции, почти не освещались в отечественной литературе. [18]
Таким образом, любое расширение выполнимой таблицы также выполнимо. Отсюда следует, что метод аналитических таблиц является непротиворечивым, из чего вытекает теорема о состоятельности этого метода. [19]
Заметим, для задания кванторов используется функциональная нотация языка Пролог. Следует отметить, что реализация метода аналитических таблиц наряду с обычными логическими связками ( &, V, - 1, -) поддерживает нетрадиционные логические связки, например, эквивалентность, стрелку Пирса и штрих Шеффера. [20]
Также очевидна непротиворечивость этого метода для логики предикатов первого порядка. Из теоремы 4.5 легко доказывается полнота метода аналитических таблиц для логики предикатов первого порядка. [21]
Метод аналитических таблиц ( или метод семантических таблиц, или метод Хинтикка) является эффективной процедурой доказательства теорем, как для логики высказываний, так и для логики предикатов первого порядка. Но если метод резолюции работает с формулами, представленными в КНФ, то метод аналитических таблиц оперирует с формулами, представленными в ДНФ. Вывод осуществляется на бинарных деревьях, вершины которых отмечены формулами, причем вершина называется концевой, если она не имеет потомков, простой, если она имеет только одного потомка и дизъюнктивной, если она имеет двух потомков. Каждая ветвь дерева представлена конъюнкцией формул, а само дерево - дизъюнкцией своих ветвей. [22]
Поскольку вслед за Фиттингом нами приведено несколько реализаций метода аналитических таблиц, зададимся вопросом: какая из реализаций является лучшей. F, где F - формула, то последняя версия предиката test является, очевидно, лучшей. Но для других типов формул эта версия предиката test является неудачной, поскольку увеличивается время на их доказуемость. Таким образом, ответ на поставленный вопрос можно дать такой: выбор лучшей реализации метода аналитических таблиц зависит от наших знаний о формуле, т.е., другими словами, эвристики здесь играют не последнюю роль. [23]
Следует отметить еще одну деталь, приводящую к неэффективности заключительной версии метода аналитических таблиц. Предположим, что аналитическая таблица построена до момента, начиная с которого она разветвляется на 5 ветвей, 4 из которых являются замкнутыми. Предикат, названный expand and close, будет тестировать на замкнутость все ветви таблицы и найдет ветвь, которая не является замкнутой. Затем применяется правило расширения таблицы, и снова вся таблица тестируется на замкнутость ветвей. Поэтому нет необходимости проверять их вновь, и более удачной версией программы является та, в которой удаляется из таблицы ветвь с обнаруженой замкнутостью. Читателю предлагается модифицировать последнюю версию реализации метода аналитических таблиц так, чтобы только что обнаруженная замкнутость ветви, удалялась из таблицы. Желаем успеха в разработке лучшей версии реализации метода аналитических таблиц для пропозициональной логики. [24]
Следует отметить еще одну деталь, приводящую к неэффективности заключительной версии метода аналитических таблиц. Предположим, что аналитическая таблица построена до момента, начиная с которого она разветвляется на 5 ветвей, 4 из которых являются замкнутыми. Предикат, названный expand and close, будет тестировать на замкнутость все ветви таблицы и найдет ветвь, которая не является замкнутой. Затем применяется правило расширения таблицы, и снова вся таблица тестируется на замкнутость ветвей. Поэтому нет необходимости проверять их вновь, и более удачной версией программы является та, в которой удаляется из таблицы ветвь с обнаруженой замкнутостью. Читателю предлагается модифицировать последнюю версию реализации метода аналитических таблиц так, чтобы только что обнаруженная замкнутость ветви, удалялась из таблицы. Желаем успеха в разработке лучшей версии реализации метода аналитических таблиц для пропозициональной логики. [25]