Реализация пролога алгоритма Куайна для классической логики высказываний (в книге Куайна «Методы логики»)
Я знаю только одну программу, которая переводит алгоритм, который Куайн дал для классической логики высказываний в своей книге « Методы логики» (Harvard University Press, 1982, гл. 1, сек. 5, стр. 33-40). здесь: алгоритм Куайна в Haskell
Я пытался перевести алгоритм Куайна на Пролог, но до сих пор мне это не удалось. Жаль, потому что это эффективный алгоритм, и перевод на Пролог был бы интересен. Я собираюсь описать этот алгоритм. Единственный код Пролога, который я привожу в начале, - это список операторов, которые были бы полезны для тестирования прувера:
% operator definitions (TPTP syntax)
:- op( 500, fy, ~). % negation
:- op(1000, xfy, &). % conjunction
:- op(1100, xfy, '|'). % disjunction
:- op(1110, xfy, =>). % conditional
:- op(1120, xfy, <=>). % biconditional
Константы истины - это topи botдля, соответственно, истина и ложь . Алгоритм начинается следующим образом: для любой пропозициональной формулы F сделайте две ее копии и замените атом, имеющий наибольшее вхождение в F, на topв первой копии и на botво второй копии, а затем примените следующие десять правил редукции: правило за раз столько раз, сколько возможно, для каждой из копий:
1. p & bot --> bot
2. p & top --> p
3. p | bot --> p
4. p | top --> p
5. p => bot --> ~p
6. p => top --> top
7. bot => p --> top
8. top => p --> p
9. p <=> bot --> ~p
10. p <=> top --> p
Конечно, у нас также есть следующие правила отрицания и двойного отрицания:
1. ~bot --> top
2. ~top --> bot
3. ~~p --> p
Когда нет ни topни botв формуле поэтому ни одно из правил не применяются, разделить его снова и выбрать один атом , чтобы заменить его top и на botв еще двух сторонней таблицы. Формула F доказана тогда и только тогда, когда алгоритм заканчивается topна всех копиях, и не может быть доказана в противном случае.
Пример:
(p => q) <=> (~q => ~p)
(p => top) <=> (bot => ~p) (p => bot) <=> (top => ~p)
top <=> top ~p <=> ~p
top top <=> top bot <=> bot
top top
Понятно, что алгоритм Куайна является оптимизацией метода таблиц истинности, но, исходя из кодов программы генератора таблиц истинности, мне не удалось получить его в коде Пролога.
Хотелось бы получить помощь хотя бы для начала. Заранее большое спасибо.
ИЗМЕНИТЬ Guy Coder
Это дважды размещено на форуме SWI-Prolog, который активно обсуждается и где пруверы Prolog публикуются, но не воспроизводятся на этой странице.
Ответы
Код на Haskell мне показался сложным. Вот реализация, основанная на описании алгоритма, приведенном в вопросе. (Используя maplistи difиз библиотеки SWI-Prolog, но легко сделать автономным.)
Во-первых, отдельные шаги упрощения:
formula_simpler(_P & bot, bot).
formula_simpler(P & top, P).
formula_simpler(P '|' bot, P).
formula_simpler(_P '|' top, top). % not P as in the question
formula_simpler(P => bot, ~P).
formula_simpler(_P => top, top).
formula_simpler(bot => _P, top).
formula_simpler(top => P, P).
formula_simpler(P <=> bot, ~P).
formula_simpler(P <=> top, P).
formula_simpler(~bot, top).
formula_simpler(~top, bot).
formula_simpler(~(~P), P).
Затем повторяющееся применение этих шагов к подтерминам и итерация в корне, пока ничего не изменится:
formula_simple(Formula, Simple) :-
Formula =.. [Operator | Args],
maplist(formula_simple, Args, SimpleArgs),
SimplerFormula =.. [Operator | SimpleArgs],
( formula_simpler(SimplerFormula, EvenSimplerFormula)
-> formula_simple(EvenSimplerFormula, Simple)
; Simple = SimplerFormula ).
Например:
?- formula_simple(~ ~ ~ ~ ~ a, Simple).
Simple = ~a.
Для замены переменных другими значениями сначала используйте предикат для поиска переменных в формулах:
formula_variable(Variable, Variable) :-
atom(Variable),
dif(Variable, top),
dif(Variable, bot).
formula_variable(Formula, Variable) :-
Formula =.. [_Operator | Args],
member(Arg, Args),
formula_variable(Arg, Variable).
При обратном отслеживании это перечислит все вхождения переменных в формуле, например:
?- formula_variable((p => q) <=> (~q => ~p), Var).
Var = p ;
Var = q ;
Var = q ;
Var = p ;
false.
Это единственный источник недетерминизма в приведенной ниже процедуре доказательства, и вы можете вставить разрез после formula_variableвызова, чтобы зафиксировать один выбор.
Теперь фактическая замена Variableв Formulaпо Replacement:
variable_replacement_formula_replaced(Variable, Replacement, Variable, Replacement).
variable_replacement_formula_replaced(Variable, _Replacement, Formula, Formula) :-
atom(Formula),
dif(Formula, Variable).
variable_replacement_formula_replaced(Variable, Replacement, Formula, Replaced) :-
Formula =.. [Operator | Args],
Args = [_ | _],
maplist(variable_replacement_formula_replaced(Variable, Replacement), Args, ReplacedArgs),
Replaced =.. [Operator | ReplacedArgs].
И, наконец, доказывающая сторона, создающая термин доказательства, подобный версии Haskell:
formula_proof(Formula, trivial(Formula)) :-
formula_simple(Formula, top).
formula_proof(Formula, split(Formula, Variable, TopProof, BotProof)) :-
formula_simple(Formula, SimpleFormula),
formula_variable(SimpleFormula, Variable),
variable_replacement_formula_replaced(Variable, top, Formula, TopFormula),
variable_replacement_formula_replaced(Variable, bot, Formula, BotFormula),
formula_proof(TopFormula, TopProof),
formula_proof(BotFormula, BotProof).
Доказательство примера из вопроса:
?- formula_proof((p => q) <=> (~q => ~p), Proof).
Proof = split((p=>q<=> ~q=> ~p),
p,
split((top=>q<=> ~q=> ~top),
q,
trivial((top=>top<=> ~top=> ~top)),
trivial((top=>bot<=> ~bot=> ~top))),
trivial((bot=>q<=> ~q=> ~bot))) .
Все его доказательства:
?- formula_proof((p => q) <=> (~q => ~p), Proof).
Proof = split((p=>q<=> ~q=> ~p), p, split((top=>q<=> ~q=> ~top), q, trivial((top=>top<=> ~top=> ~top)), trivial((top=>bot<=> ~bot=> ~top))), trivial((bot=>q<=> ~q=> ~bot))) ;
Proof = split((p=>q<=> ~q=> ~p), p, split((top=>q<=> ~q=> ~top), q, trivial((top=>top<=> ~top=> ~top)), trivial((top=>bot<=> ~bot=> ~top))), trivial((bot=>q<=> ~q=> ~bot))) ;
Proof = split((p=>q<=> ~q=> ~p), q, trivial((p=>top<=> ~top=> ~p)), split((p=>bot<=> ~bot=> ~p), p, trivial((top=>bot<=> ~bot=> ~top)), trivial((bot=>bot<=> ~bot=> ~bot)))) ;
Proof = split((p=>q<=> ~q=> ~p), q, trivial((p=>top<=> ~top=> ~p)), split((p=>bot<=> ~bot=> ~p), p, trivial((top=>bot<=> ~bot=> ~top)), trivial((bot=>bot<=> ~bot=> ~bot)))) ;
Proof = split((p=>q<=> ~q=> ~p), q, trivial((p=>top<=> ~top=> ~p)), split((p=>bot<=> ~bot=> ~p), p, trivial((top=>bot<=> ~bot=> ~top)), trivial((bot=>bot<=> ~bot=> ~bot)))) ;
Proof = split((p=>q<=> ~q=> ~p), q, trivial((p=>top<=> ~top=> ~p)), split((p=>bot<=> ~bot=> ~p), p, trivial((top=>bot<=> ~bot=> ~top)), trivial((bot=>bot<=> ~bot=> ~bot)))) ;
Proof = split((p=>q<=> ~q=> ~p), p, split((top=>q<=> ~q=> ~top), q, trivial((top=>top<=> ~top=> ~top)), trivial((top=>bot<=> ~bot=> ~top))), trivial((bot=>q<=> ~q=> ~bot))) ;
Proof = split((p=>q<=> ~q=> ~p), p, split((top=>q<=> ~q=> ~top), q, trivial((top=>top<=> ~top=> ~top)), trivial((top=>bot<=> ~bot=> ~top))), trivial((bot=>q<=> ~q=> ~bot))) ;
false.
Это содержит много избыточности. Опять же, это потому, что formula_variableперечисляет вхождения переменных. Его можно сделать более детерминированным различными способами в зависимости от требований.
РЕДАКТИРОВАТЬ: Вышеупомянутая реализация formula_simpleнаивна и неэффективна: каждый раз, когда она делает успешное упрощение в корне формулы, она также пересматривает все подформулы. Но в этой задаче никакие новые упрощения подформул не станут возможными при упрощении корня. Вот новая версия, которая более осторожна: сначала полностью переписывает подформулы, а затем выполняет итерацию перезаписи только в корне:
formula_simple2(Formula, Simple) :-
Formula =.. [Operator | Args],
maplist(formula_simple2, Args, SimpleArgs),
SimplerFormula =.. [Operator | SimpleArgs],
formula_rootsimple(SimplerFormula, Simple).
formula_rootsimple(Formula, Simple) :-
( formula_simpler(Formula, Simpler)
-> formula_rootsimple(Simpler, Simple)
; Simple = Formula ).
Это значительно быстрее:
?- time(formula_simple(~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~(a & b & c & d & e & f & g & h & i & j & k & l & m & n & o & p & q & r & s & t & u & v & w & x & y & z), Simple)).
% 11,388 inferences, 0.004 CPU in 0.004 seconds (100% CPU, 2676814 Lips)
Simple = ~ (a&b&c&d&e&f&g&h& ... & ...).
?- time(formula_simple2(~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~(a & b & c & d & e & f & g & h & i & j & k & l & m & n & o & p & q & r & s & t & u & v & w & x & y & z), Simple)).
% 988 inferences, 0.000 CPU in 0.000 seconds (100% CPU, 2274642 Lips)
Simple = ~ (a&b&c&d&e&f&g&h& ... & ...).
Изменить: как указано в комментариях, прувер, как написано выше, может быть очень медленным на немного больших формулах. Проблема в том, что я забыл, что некоторые операторы коммутативны! Спасибо jnmonette за указание на это. Правила перезаписи нужно немного расширить:
formula_simpler(_P & bot, bot).
formula_simpler(bot & _P, bot).
formula_simpler(P & top, P).
formula_simpler(top & P, P).
formula_simpler(P '|' bot, P).
formula_simpler(bot '|' P, P).
...
И с этим прувер хорошо себя ведет.
Вот скелет решения. Я надеюсь, что это поможет вам заполнить пробелы.
is_valid(Formula) :-
\+ derive(Formula,bot).
is_satisfiable(Formula) :-
derive(Formula, top).
derive(bot,D):-
!,
D=bot.
derive(top,D):-
!,
D=top.
derive(Formula,D):-
reduce(Formula, Formula1),
(
Formula=Formula1
->
branch(Formula1,D)
;
derive(Formula1,D)
).
Теперь вам нужно реализовать reduce / 2, которое применяет правила сокращения (рекурсивно в подформулах), и branch / 2, которая недетерминированно заменяет атом формулы на top или bot, а затем рекурсивно вызывает derive / 2. Что-то вроде:
branch(Formula, D):-
pickAtom(Formula, Atom),
(
Rep=top
;
Rep=bot
),
replace(Formula, Atom, Rep, Formula1),
derive(Formula1,D).
Похоже, этот метод грубой силы старше (*), а поскольку код Пролога настолько мал, что он даже помещается в карман ваших брюк:
Вот полная реализация. Сокращение используется только для определения приоритета перезаписи и в значительной степени соответствует правилам Haskell. За исключением того, что в Haskell может не быть логической переменной типа данных, такой как Prolog:
:- op(300, fy, ~).
eval(A, A) :- var(A), !.
eval(A+B, R) :- !, eval(A, X), eval(B, Y), simp(X+Y, R).
eval(A*B, R) :- !, eval(A, X), eval(B, Y), simp(X*Y, R).
eval(~A, R) :- !, eval(A, X), simp(~X, R).
eval(A, A).
simp(A, A) :- var(A), !.
simp(A+B, B) :- A == 0, !.
simp(A+B, A) :- B == 0, !.
simp(A+_, 1) :- A == 1, !.
simp(_+B, 1) :- B == 1, !.
simp(A*_, 0) :- A == 0, !.
simp(_*B, 0) :- B == 0, !.
simp(A*B, B) :- A == 1, !.
simp(A*B, A) :- B == 1, !.
simp(~A, 1) :- A == 0, !.
simp(~A, 0) :- A == 1, !.
simp(A, A).
Код не является чистым Прологом и использует нелогическое метапрограммирование var / 1, (==) / 2 и т. Д. Как и Boole, мы линейно уменьшаем и выполняем соединение двух замен, поэтому мы делаем разбиение Куайна без некоторого ветвления и через один фронт:
judge(A, [B|R]) :- eval(A, B),
term_variables(B, L), judge(B, L, R).
judge(_, [], R) :- !, R = [].
judge(A, [B|L], R) :-
copy_term(A-[B|L], C-[0|L]),
copy_term(A-[B|L], D-[1|L]), judge(C*D, R).
Выше мы использовали copy_term / 2 для подстановки. Идея позаимствована из лямбда-библиотеки Ульриха Ноймеркельса. Нам также нужно сделать доступными = <и =: = в eval / 2 и simp / 2. Полный исходный код см. Здесь . Вот примеры прогонов в любом из ваших любимых ISO Prolog:
?- judge(A+ ~A, L).
L = [A+ ~A, 1] /* Ends in 1, Tautology */
?- judge(A+ ~B, L).
L = [A+ ~B, ~B, 0] /* Ends in 0, Falsifiable */
?- judge(((P+Q)=<R)=:=((P=<R)*(Q=<R)), L).
L = [(P+Q =< R) =:= (P =< R)*(Q =< R),
((Q =< R) =:= (Q =< R))*(R =:= R*(Q =< R)),
(R =:= R)*((R =:= R)*(R =:= R*R)), 1].
(*) От:
У. Мартин и Т. Нипков. Логическое объединение - история до сих пор.
В Unification, страницы 437–455. Академик Пресс, Лондон, 1990.