Вывод в исчислении высказываний

Автоматический вывод формул списка Targets из формул списка Axioms при помощи правила modus ponens. В формулах разрешены только импликация и отрицание. Реализовано два метода поиска "от аксиом" и "от цели".

В методе "от аксиом" может быть произвольное число целевых формул. Как только какой нибудь вывод найден, целевая формула убирается из списка. Метод хорош для быстрого поиска большого числа выводов, не всегда оптимальных по длине. Параметр maxImp отбрасывает формулы с большей длиной (по числу импликаций). Рекомендуется этот параметр начинать постепенно увеличивать, после окончания поиска (исчерпались все циклы maxCycles или вывод не найден).

Второй метод ("от цели") ищет вывод только к одной целевой формуле (первой). Но при этом перебирает различные варианты выводов, показывая лучший по длине (len) и по максимально длинной формуле (imp) Параметр maxDepth контролирует максимальную глубину дерева вывода, а maxNodes число в нём улов. Деревья с большими значениями отбрасываются. Если вывод не найден, эти параметры стоит увеличить. Заметим, что в общем случае maxNodes может быть существенно больше длины вывода (len), если в его дереве есть повторяющиеся ветки.

Axioms:
Targets:
Метод поиска:
От аксиом: maxImp : , maxCycles : , maxWords : ,
добавить правило RT
От цели: maxNodes : , maxDepth : , maxProofs : ,
Эвристика:
Reference:
P->(Q->P); #F1;
(P->(Q->R))->((P->Q)->(P->R)); #F2;
(P->Q)->((Q->R)->(P->R)); #T;
(P->(Q->R))->(Q->(P->R)); #C;
(P->Q)->((R->P)->(R->Q)); #TC;
((P->Q)->P)->P; #P;
P->(((Q->R)->Q)->Q); #PP;
((P->(Q->R))->Q)->Q; #PA;
((P->Q)->P)->(R->P); #PB;
P->P; #I;
(P->(P->Q))->(P->Q); #I1;
(P->Q)->(P->(R->Q)); #I2;
P->((Q->R)->((P->Q)->R)); #I3;
(P->Q)->(((P->R)->Q)->Q); #A1;
((P->Q)->R)->((P->R)->R); #A2;
P->(Q->(R->P)); #S1;
((P->Q)->R)->((R->P)->(S->P)); #L1;
(P->Q)->(!Q->!P); #F3;
!!P->P; #F4;
P->!!P; #F5;
(!P->!Q)->(Q->P); #L;
P->(!P->Q); #L2;
(!P->P)->P; #L3;


Нажми на меня