Автоматический поиск натурального вывода: история вопроса

Относительно завершенного вывода (завершенного доказательства) в системе натурального вывода предлагается доказательство утверждения о семантической непротиворечивости (Теорема 2.2.4), т.е. в произвольном завершенном выводе (доказательстве) между посылками и заключением имеет место отношение логического следования. Таким образом, всякая формула, доказуемая в системе, общезначима.

Доказательство теоремы о семантической непротиворечивости системы опирается на предложенное У. Куайном доказательство теоремы о семантической непротиворечивости.

Отметим, что в системе У. Куайна (а значит, в предложенном им доказательстве теоремы о семантической непротиворечивости) существенным образом используется алфавитный порядок, заданный на множестве используемых в языке переменных.

Система BMV не предполагает наличие алфавитного порядка на множестве используемых в выводе переменных. Поэтому доказательство теоремы о семантической непротиворечивости системы натурального вывода, предложенное У. Куайном, не обобщается на систему BMV.

В связи с этим вводится понятие пассивной переменной в BMV-выводе (доказательстве), т.е. такой абсолютно ограниченной переменной в BMV-выводе (доказательстве), которая не ограничивает относительно ни одну абсолютно ограниченную переменную данного BMV-вывода (доказательства).²²

Показывается, что в произвольном алго-выводе всегда найдется пассивная переменная (Лемма 2.2.4).

Далее предлагается алгоритм поиска вывода в данном исчислении, который является модификацией алгоритма поиска натурального вывода, разработанного В.А. Бочаровым, А.Е. Болотовым и А.Е. Горчаковым.

С использованием теоремы о семантической непротиворечивости системы натурального вывода BMV показывается, что данный алгоритм обладает свойством семантической непротиворечивости, поскольку каждый вывод (доказательство), полученный алгоритмом, является выводом (доказательством) в системе BMV (Теорема 4.1.2).

Понятие вывода (доказательства) в системе BMV предполагает, что в выводе (доказательстве) ни одна переменная не ограничивает сама себя. Переменная ограничивает другую переменную согласно формулировкам правил V_B, З_и.

Экспликация отношения ограничения показывает, что данное отношение, заданное на множестве переменных вывода (доказательства), обладает свойствами иррефлексивности (ни одна переменная не ограничивает сама себя) и транзитивности (если переменная х ограничивает переменную у и переменная у ограничивает z, то переменная х ограничивает переменную z).

Таким образом, отношение ограничения, заданное на множестве переменных вывода (доказательства), является отношением строгого (частичного) порядка.

В силу того, что теория строгого порядка разрешима, процедура проверки, ограничивает ли произвольная переменная сама себя, конечна для произвольного завершенного вывода (доказательства).

Встроенный в алгоритм поиска вывода стандартный алгоритм унификации адаптирован для работы с абсолютно и относительно ограниченными переменными и содержит вышеупомянутую процедуру поиска в выводе (доказательстве) переменной, которая ограничивает сама себя.

Минимальной единицей алгоритмического вывода является блок - непустая, конечная последовательность формул. Последовательность блоков образует собой древовидную структуру - дерево поиска вывода, в котором переход от одного блока к другому осуществляется с помощью правил поиска вывода.

Показывается конечность ветвления для произвольного блока в произвольном дереве поиска вывода (Лемма 4.3.1).

Опираясь на представление алгоритмического натурального вывода в виде древовидной структуры, выделяется некоторая нить данного дерева, множество формул в которой образует множество Хинтикки (модельное множество).

Таким образом, если для некоторой выводимости формулы из (возможно, пустого) множества посылок невозможно построить алгоритмический вывод, то данная формула логически не следует из данного множества посылок и алгоритмический вывод содержит (возможно, бесконечную) контрмодель, т.е. такую интерпретацию, при которой все формулы из данного множества посылок принимают значение «истина», а данная формула принимает значение «ложь».

Отсюда следует по контрапозиции, что предложенный алгоритм поиска натурального вывода типа Куайна в классической логике предикатов первого порядка обладает свойством семантической полноты, т.е. для любой общезначимой формулы классической логики предикатов можно построить вывод в предложенном алгоритме (Теорема 4.3.7).

Поскольку всякий алгоритмический вывод есть вывод в системе BMV, из утверждения о семантической полноте алгоритма следует утверждение о семантической полноте системы BMV (Теорема 4.3.8).

В ходе исследования обнаружены следующие проблемы, требующие дальнейшей разработки:

а) теорема о семантической полноте системы BMV тривиально следует из теоремы о семантической полноте алгоритма поиска вывода в системе BMV. Однако остается невыясненной возможность прямого, а не косвенного доказательства теоремы о семантической полноте системы BMV (например, установлением факта, что все, что доказуемо в стандартном гильбертовском исчислении, имеет завершенное доказательство в системе BMV).

b) обобщение изложенного алгоритма и прямого метода доказательства теоремы о семантической полноте на неклассические логики предикатов (интуиционистскую, релевантную и др.)- Учитывая, что пропозициональный вариант алгоритма для классической логики обобщается на интуиционистскую логику высказываний, выдвигается гипотеза, что указанные в работе методы применимы к неклассическим логикам предикатов.

c) решение для предложенного алгоритма проблемы поиска минимальных контрмоделей: если некоторая формула имеет как конечную, так и бесконечную контрмодель, то в процессе поиска вывода алгоритм не всегда предлагает конечную контрмодель. При этом предполагается, что построение алгоритмом бесконечной контрмодели в случае, если имеется возможность построения конечной контрмодели, неэффективно с точки зрения вычислимости.

d) создание машинной реализации для данного алгоритма в виде компьютерной программы, которая позволит облегчить усвоение и запоминание основ дедукции.

Список использованных источников и литературы

1. Andrews P. Transforming matings into natural deduction proofs // 5^th Conference on Automated Deduction. ? 1980.

2. Basin D., Matthews S., Vigano L. Natural deduction for non-classical logics // Studia Logica. ? vol. 60. ? №1. ? 1998.

3. Bocharov V., Bolotov A., Gorchakov A., Shangin V. Proof-searching algorithm in first order classical natural deduction calculus // 12^th International Congress of Logic, Methodology and Philosophy of Science. Oviedo (Spain), August 7-13, 2003.

4. Bochmann G. Hardware specification with temporal logic: an example // IEEE Transactions on computers. ? vol. C-31. ? №3. ? 1982.

5. Bolotov A., Fisher M. A resolution method for computational tree branching time temporal logic // rV International workshop on temporal representation and reasoning (TIME'97). ? Florida, 1997.

6. Byrnes J. Proof search and normal forms in natural deduction. PhD thesis. ? Pittsburgh, 1999.

7. Church A. A note on the Entscheidungsproblem // The Journal of Symbolic Logic. ? vol. 1. ? №1. ? 1936.

8. Church A. Correction to A note on the Entscheidungsproblem // The Journal of Symbolic Logic. ? vol. 1. ? №3. ? 1936.

9. Copi I. Symbolic logic. 3^rd ed. ? New-York, London, 1967.

10. Fitch F. Symbolic logic. ? New York, 1952.

11. Hintikka J. A new approach to sentential logic // Societas Scientarium Fennica Commentationes Physico-Mathematicae XVII. - №2. ? 1957.

12. Hintikka J. Notes on the quantification theory // Societas Scientarium Fennica Commentationes Physico-Mathematicae XVII. ? №11. ? 1957.

13. Jaskowski S. On the rules of suppositions in formal logic // Studia Logica. ? №1. ? 1934.

14. Kalish D. Review of Copi: Symbolic logic. 3^rd ed. New-York, London, 1967. // The Journal of Symbolic Logic. ? vol. 39. ? №1. ? 1974.

Размещено на Allbest.ru