การนำอัลกอริทึมของ Quine ไปใช้ Prolog สำหรับตรรกะเชิงประพจน์แบบคลาสสิก (ใน Quine's "Methods of Logic")
ฉันรู้เพียงสุภาษิตเดียวที่แปลอัลกอริทึมที่ Quine มอบให้สำหรับตรรกศาสตร์เชิงประพจน์คลาสสิกในหนังสือMethods of Logic (Harvard University Press, 1982, ch. 1 sec. 5, pp. 33-40) สุภาษิตนี้อยู่ใน Haskell และมัน อยู่ที่นี่: อัลกอริทึมของ Quine ใน Haskell
ฉันพยายามแปลอัลกอริทึมของ Quine ใน Prolog แต่จนถึงตอนนี้ฉันยังไม่ประสบความสำเร็จ เป็นที่น่าเสียดายเพราะเป็นอัลกอริทึมที่มีประสิทธิภาพและการแปล Prolog ก็น่าสนใจ ฉันจะอธิบายอัลกอริทึมนี้ รหัส Prolog เดียวที่ฉันให้ตอนเริ่มต้นคือรายชื่อตัวดำเนินการที่จะเป็นประโยชน์ในการทดสอบสุภาษิต:
% 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
เป็นที่ชัดเจนว่าอัลกอริทึมของ Quine เป็นการเพิ่มประสิทธิภาพของวิธีตารางความจริง แต่เริ่มจากรหัสของโปรแกรมสร้างตารางความจริงฉันไม่ประสบความสำเร็จในการรับมันในรหัส Prolog
ความช่วยเหลืออย่างน้อยในการเริ่มต้นก็ยินดีต้อนรับ ล่วงหน้าขอบคุณมาก
แก้ไขโดย Guy Coder
นี่คือโพสต์สองครั้งที่ฟอรัม SWI-Prolog ซึ่งมีการอภิปรายที่มีชีวิตชีวาและเป็นที่ที่มีการเผยแพร่ Provers 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)
).
ตอนนี้คุณต้องใช้การลด / 2 ที่ใช้กฎการลด (แบบวนซ้ำในสูตรย่อย) และ branch / 2 ที่แทนที่อะตอมของสูตรที่ไม่ได้กำหนดด้วยปัจจัยด้านบนหรือบอทจากนั้นเรียกแบบเรียกซ้ำ / 2 สิ่งที่ต้องการ:
branch(Formula, D):-
pickAtom(Formula, Atom),
(
Rep=top
;
Rep=bot
),
replace(Formula, Atom, Rep, Formula1),
derive(Formula1,D).
ดูเหมือนว่าวิธี brute force นี้เก่ากว่า (*) และเนื่องจากรหัส Prolog มีขนาดเล็กมากจึงสามารถใส่ลงในกระเป๋ากางเกงได้ด้วย:
นี่คือการใช้งานเต็มรูปแบบ การตัดใช้เพื่อจัดลำดับความสำคัญของการเขียนใหม่เท่านั้นและสอดคล้องกับกฎของ 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).
รหัสไม่ใช่ Prolog ที่บริสุทธิ์และใช้ var / 1 ที่ไม่ใช่ตรรกะ (==) / 2 ฯลฯ .. การเขียนโปรแกรมเมตา เช่นเดียวกับ Boole เราลดและดำเนินการร่วมกันของการแทนที่ทั้งสองแบบเป็นเส้นตรงดังนั้นเราจึงทำการแยก Quine โดยไม่แยกส่วนและผ่านด้านหน้าเดียว:
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 เพื่อทำการทดแทน แนวคิดนี้ยืมมาจากห้องสมุด Ulrich Neumerkels lambda เราจำเป็นต้องทำให้พร้อมใช้งาน = <และ =: = ใน 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].
(*) จาก:
U. Martin และ T. Nipkow การรวมบูลีน - เรื่องราวจนถึงตอนนี้
ใน Unification หน้า 437–455 สำนักพิมพ์วิชาการลอนดอน 2533