Implementasi prolog dari algoritma Quine untuk logika proposisional klasik (dalam "Metode Logika" Quine)
Saya hanya tahu satu pepatah yang menerjemahkan algoritme yang diberikan Quine untuk logika proposisional klasik dalam bukunya Methods of Logic (Harvard University Press, 1982, ch. 1 sec. 5, hlm. 33-40), pepatah ini ada di Haskell dan itu di sini: Algoritme Quine di Haskell
Saya mencoba menerjemahkan algoritma Quine di Prolog, namun sampai saat ini saya belum berhasil. Sangat disayangkan karena ini adalah algoritma yang efisien dan terjemahan Prolog akan menarik. Saya akan menjelaskan algoritma ini. Satu-satunya kode Prolog yang saya berikan di awal adalah daftar operator yang akan berguna untuk menguji prover:
% operator definitions (TPTP syntax)
:- op( 500, fy, ~). % negation
:- op(1000, xfy, &). % conjunction
:- op(1100, xfy, '|'). % disjunction
:- op(1110, xfy, =>). % conditional
:- op(1120, xfy, <=>). % biconditional
Konstanta kebenaran adalah topdan botuntuk, masing-masing, benar dan salah . Algoritma dimulai sebagai berikut: Untuk setiap rumus proposisi F , membuat dua salinan itu dan menggantikan atom yang memiliki terjadinya tertinggi di F oleh topdi copy pertama, dan oleh botdi salinan kedua, dan kemudian menerapkan pengurangan sepuluh berikut aturan salah satu aturan pada waktu sebanyak mungkin, untuk setiap salinan:
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
Tentu saja, kami juga memiliki aturan berikut untuk negasi dan negasi ganda:
1. ~bot --> top
2. ~top --> bot
3. ~~p --> p
Jika tidak ada topatau botdalam rumus sehingga tidak ada aturan yang berlaku, pisahkan lagi dan pilih satu atom untuk menggantikannya dengan top dan oleh botdi tabel dua sisi lainnya. Rumus F dibuktikan jika dan hanya jika algoritme diakhiri dengan topdi semua salinan, dan gagal dibuktikan, sebaliknya.
Contoh:
(p => q) <=> (~q => ~p)
(p => top) <=> (bot => ~p) (p => bot) <=> (top => ~p)
top <=> top ~p <=> ~p
top top <=> top bot <=> bot
top top
Jelas bahwa algoritma Quine merupakan optimasi dari metode tabel kebenaran, namun mulai dari kode program generator tabel kebenaran, saya tidak berhasil mendapatkannya dalam kode Prolog.
Bantuan setidaknya untuk memulai akan diterima. Sebelumnya, terima kasih banyak.
EDIT oleh Guy Coder
Ini diposting ganda di forum SWI-Prolog yang memiliki diskusi yang hidup dan di mana Prolog Prolog diterbitkan tetapi tidak direproduksi di halaman ini.
Jawaban
Kode Haskell tampak rumit bagi saya. Berikut implementasi berdasarkan deskripsi algoritma yang diberikan dalam pertanyaan. (Menggunakan maplistdan difdari pustaka SWI-Prolog, tetapi mudah dibuat mandiri.)
Pertama, langkah penyederhanaan tunggal:
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).
Kemudian, aplikasi ulang langkah-langkah ini ke subterms dan iterasi di root hingga tidak ada perubahan lagi:
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 ).
Sebagai contoh:
?- formula_simple(~ ~ ~ ~ ~ a, Simple).
Simple = ~a.
Untuk penggantian variabel dengan nilai lain, pertama predikat untuk menemukan variabel dalam rumus:
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).
Saat mundur, ini akan menghitung semua kemunculan variabel dalam rumus, misalnya:
?- formula_variable((p => q) <=> (~q => ~p), Var).
Var = p ;
Var = q ;
Var = q ;
Var = p ;
false.
Ini adalah satu-satunya sumber nondeterminisme dalam prosedur pembuktian di bawah, dan Anda dapat menyisipkan potongan setelah formula_variablepanggilan untuk berkomitmen pada satu pilihan.
Sekarang penggantian a Variabledi a Formulaoleh 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].
Dan terakhir pembuktian, membangun istilah pembuktian seperti versi 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).
Bukti contoh dari pertanyaan:
?- 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))) .
Semua buktinya:
?- 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.
Ini mengandung banyak redundansi. Sekali lagi, ini karena formula_variablemenghitung kemunculan variabel. Itu dapat dibuat lebih deterministik dengan berbagai cara tergantung pada kebutuhan seseorang.
EDIT: Penerapan di atas formula_simplenaif dan tidak efisien: Setiap kali berhasil membuat penyederhanaan pada akar rumus, ia juga meninjau kembali semua subformula. Tetapi pada masalah ini, tidak ada penyederhanaan baru dari subformula yang akan dimungkinkan ketika root disederhanakan. Berikut ini versi baru yang lebih berhati-hati untuk terlebih dahulu menulis ulang subformula sepenuhnya, lalu hanya mengulang penulisan ulang di root:
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 ).
Ini jauh lebih cepat:
?- 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& ... & ...).
Edit: Seperti yang ditunjukkan di komentar, pepatah seperti yang tertulis di atas bisa sangat lambat pada rumus yang sedikit lebih besar. Masalahnya adalah saya lupa bahwa beberapa operator bersifat komutatif! Terima kasih jnmonette untuk menunjukkan hal ini. Aturan penulisan ulang harus diperluas sedikit:
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).
...
Dan dengan ini pepatah berperilaku baik.
Inilah kerangka solusi. Saya harap ini dapat membantu Anda mengisi lubang.
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)
).
Sekarang Anda perlu mengimplementasikan pengurangan / 2 yang menerapkan aturan pengurangan (secara rekursif dalam sub-rumus), dan cabang / 2 yang secara non-deterministik menggantikan atom rumus dengan top atau bot, lalu memanggil secara rekursif derive / 2. Sesuatu seperti:
branch(Formula, D):-
pickAtom(Formula, Atom),
(
Rep=top
;
Rep=bot
),
replace(Formula, Atom, Rep, Formula1),
derive(Formula1,D).
Tampaknya metode brute force ini lebih tua (*), dan karena kode Prolognya sangat kecil, bahkan muat di saku celana Anda:
Berikut adalah implementasi lengkapnya. Pemotongan hanya digunakan untuk memprioritaskan penulisan ulang dan sesuai dengan banyak aturan Haskell. Kecuali bahwa Haskell mungkin tidak memiliki variabel logis tipe data seperti 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).
Kode tersebut bukan Prolog murni dan menggunakan non-logis var / 1, (==) / 2, dll .. meta pemrograman. Seperti Boole, kami secara linier mengurangi dan melakukan konjungsi dari dua substitusi, jadi kami melakukan pemisahan Quine tanpa beberapa percabangan dan melalui satu front:
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).
Di atas kami menggunakan copy_term / 2 untuk melakukan substitusi. Ide tersebut dipinjam dari perpustakaan lambda Ulrich Neumerkels. Kita juga perlu menyediakan = <dan =: = di eval / 2 dan simp / 2. Untuk kode sumber lengkap lihat di sini . Berikut adalah contoh berjalan di salah satu Prolog ISO favorit Anda:
?- 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].
(*) Dari:
U. Martin dan T. Nipkow. Unifikasi Boolean — sejauh ini ceritanya.
Dalam Unification, halaman 437–455. Academic Press, London, 1990.