2014 dxdy logo

Научный форум dxdy

Математика, Физика, Computer Science, Machine Learning, LaTeX, Механика и Техника, Химия,
Биология и Медицина, Экономика и Финансовая Математика, Гуманитарные науки


Правила форума


Посмотреть правила форума



Начать новую тему Ответить на тему
 
 Алгоритм формального вывода в ИВ
Сообщение20.04.2019, 14:15 


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

 Профиль  
                  
 
 Re: Алгоритм формального вывода в ИВ
Сообщение20.04.2019, 16:22 
Заслуженный участник


27/04/09
28128
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$), но никогда не построит последовательность формул, не являющуюся выводом (ну, если понят и реализован правильно).

 Профиль  
                  
 
 Re: Алгоритм формального вывода в ИВ
Сообщение20.04.2019, 19:42 
Заслуженный участник


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

 Профиль  
                  
 
 Re: Алгоритм формального вывода в ИВ
Сообщение20.04.2019, 20:15 
Заслуженный участник


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

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

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

 Профиль  
                  
 
 Re: Алгоритм формального вывода в ИВ
Сообщение20.04.2019, 21:47 
Заслуженный участник


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

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

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

 Профиль  
                  
 
 Re: Алгоритм формального вывода в ИВ
Сообщение21.04.2019, 20:48 


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

 Профиль  
                  
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему  [ Сообщений: 6 ] 

Модераторы: Модераторы Математики, Супермодераторы



Кто сейчас на конференции

Сейчас этот форум просматривают: Vladimir Pliassov


Вы не можете начинать темы
Вы не можете отвечать на сообщения
Вы не можете редактировать свои сообщения
Вы не можете удалять свои сообщения
Вы не можете добавлять вложения

Найти:
Powered by phpBB © 2000, 2002, 2005, 2007 phpBB Group