Алгоритм формального вывода в ИВ

[Vadimovich]

Добрый день. Стоит задача написать программу, которая будет строить формальный вывод теоремы. Использовать можно стандартные аксиомы L и modus ponens.
Подскажите идею, алгоритмы и вообще куда двигаться, что читать, что гуглить. Я пока ничего толкового найти не сумел. Перебор не годится, так как съедает память в две секунды.
Спасибо!

[arseniiv]

Vadimovich в сообщении #1388701 писал(а):

стандартные аксиомы L

…которые, кстати, всё-таки бывают разными в зависимости от учебника. Например, одни авторы стремятся к минимализму и делают формулы со связками $\wedge,\vee,\leftrightarrow$ сокращениями формул со связками только $\to,\neg$, другие желают, чтобы (производные) правила введения и удаления связок получались из аксиом в пару шагов, и потому аксиом много и т. п.. Это может в частности немного менять, насколько простым может быть алгоритм.

Вообще же можно сделать довольно грубо, но действенно. Пусть в формулу $F$ входят переменные $A_1,\ldots,A_n$. Сначала выводим $A\to B,\neg A\to B\vdash B$, этот вывод будет использоваться как клей, которым алгоритм будет склеивать $2^n$ выводов формул $[\neg]A_1\to\ldots\to[\neg]A_n\to F$ (по всем вариантам расстановки $\neg$). Сами эти выводы можно получить, используя теорему о дедукции и всевозможные «правила таблицы истинности» $[\neg]A, [\neg]B\vdash [\neg]A*B$, где $*$ — разные двухместные связки (для отрицания не понадобится), собирая с помощью них формулу из каждого набора гипотез $[\neg]A_1,\ldots,[\neg]A_n$. Тут можно найти оптимизации, но чем проще алгоритм, тем ведь быстрее его корректная реализация?

Схема выше хороша ещё и тем, что она как раз не зависит от конкретного вида набора связок и аксиом — от него зависит то, какие выводы породит теорема о дедукции и какие выводы мы сделаем для «правил таблицы истинности» и $A\to B,\neg A\to B\vdash B$, а вот сборка будет одна и та же. Ещё этот алгоритм не сработает для не-теоремы (потому что в построении одного из выводов соберётся не $F$, а $\neg F$), но никогда не построит последовательность формул, не являющуюся выводом (ну, если понят и реализован правильно).

[george66]

Поищите на слова "метод резолюций", но хорошего ресурса не знаю, поскольку не интересовался.

[arseniiv]

Из вывода методом резолюций классический тоже трудно будет создавать. («Тоже» — потому что схема выше — это приукрашенная проверка таблицы истинности.)

-- Сб апр 20, 2019 22:24:28 --

Если же говорить о «негильбертовских» методах подетерминированнее и притом не взрывающихся во многих хороших случаях, есть sequent calculus и analytic tableaux (как я понял, это почти одно и то же).

[Yuri Gendelman]

Чень Ч., Ли Р. "Математическая логика и автоматическое доказательство теорем". 1983
(Оригинал: "Symbolic Logic and Mechanical Theorem Proving" by Chin-Liang Chang, Richard Char-Tung Lee. 1973)

Очень подробно описывается метод резолюций.
Приведен текст программы на Lisp.

P.S. Метод резолюций предназначен для логики 1-го порядка. В ИВ все должно быть проще.

[Sender]

Боюсь, если говорить о практическом применении, наивное применение метода резолюций тоже в два счёта сожрёт всю доступную память. Возможно, имеет смысл ознакомиться с алгоритмом CDCL.