在序言truthtable分裂

Question

你好計算器社區

，所以我試圖計算此輸出

A      B     and(A,B)  or(A,and(A,B))  
true    true    true    true     
true    true    false    false    
false    false    true    false    
false    false    false    false 

但是我的代碼給我的錯誤，當我諮詢一下吧

這裏是我的代碼

:- use_module(library(apply)). 


    and(A,B) :- A, B. 

    or(A,_) :- A. 
    or(_,B) :- B. 

    equ(A,B) :- or(and(A,B), and(not(A),not(B))). 

    xor(A,B) :- not(equ(A,B)). 

    nor(A,B) :- not(or(A,B)). 

    nand(A,B) :- not(and(A,B)). 

    impl(A,B) :- or(not(A),B). 


    :- op(900, fy,not). 
    :- op(910, yfx, and). 
    :- op(910, yfx, nand). 
    :- op(920, yfx, or). 
    :- op(920, yfx, nor). 
    :- op(930, yfx, impl). 
    :- op(930, yfx, equ). 
    :- op(930, yfx, xor). 


    eval(Bindings, X, V) --> 
     {var(X)}, 
     !, 
     {get_binding(Bindings, X, V)}, 
     [X-V]. 
    eval(Bindings, Term, V) --> 
     {compound(Term)}, 
     !, 
     {Term =.. [Op|Args]}, 
     evals(Bindings, Args, Values), 
     { 
      GroundTerm =.. [Op|Values], 
      (GroundTerm -> V = true ; V = false) 
     }, 

     [Term - V]. 
    eval(_Bindings, Term) --> 
     % Term is nonvar atomic 
     {domain_error(either(var, compound), Term)}. 

    evals(_Bindings, [], []) --> 
     !, 
     []. 
    evals(Bindings, [A|As], [V|Vs]) --> 
     eval(Bindings, A, V), 
     evals(Bindings, As, Vs). 

    get_binding([Var0-Val0|Bindings], V, Val) :- 
     (V == Var0 -> 
      Val = Val0 
     ; 
     get_binding(Bindings, V, Val) 
     ). 
    get_binding([], V, _) :- 
     throw(error(missing_binding_for(V), _)). 


    valuations(N, Valuations) :- 
     findall(Valuation, 
       valuation(N, Valuation), 
       Valuations). 

    valuation(0, []) :- !. 
    valuation(N, [V|Vs]) :- 
     succ(N0, N), 
     member(V, [true, false]), 
     valuation(N0, Vs). 


    bindings(Vars, Bindings) :- 
     length(Vars, N), 
     valuations(N, Valuations), 
     maplist({Vars}/[X, Y] >> pairs_keys_values(Y, Vars, X), Valuations, Bindings). 


    compute_tt(Expr, TruthTable) :- 
     term_variables(Expr, Vars), 
     bindings(Vars, Bindings), 
     maplist({Expr}/[Binding, Row]>>phrase(eval(Binding, Expr, _), Row, []), Bindings, Rows), 

     Rows = [Row|_], 
     pairs_keys(Row, Header), 
     maplist(pairs_values, Rows, Rows1), 
     TruthTable = [Header|Rows1]. 

    print_tt_row(Row) :- 
     forall(member(El, Row), 
       format('~|~p~20+', [El])), 
     nl. 


    print_tt(TruthTable) :- 
     numbervars(TruthTable, 0, _), 
     maplist(print_tt_row, TruthTable). 

諮詢時出錯

Warning: [Thread pce] The predicates below are not defined. If these are defined 
Warning: [Thread pce] at runtime using assert/1, use :- dynamic Name/Arity. 
Warning: [Thread pce] 
Warning: [Thread pce] >>/4, which is referenced by 
Warning: [Thread pce]1-st clause of bindings/2 
Warning: [Thread pce]1-st clause of compute_tt/2 

藏漢作爲一個錯誤，當我鍵入一個聲明

1 ?- 
| compute_tt(or(X, and(X, Y)), TT), print_tt(TT). 
ERROR: apply:maplist_/3: Undefined procedure: (>>)/4 
    Exception: (12) >>({[_G1821, _G1822]}/[_G2035, _G2038], pairs_keys_values(_G2038, [_G1821, _G1822], _G2035), [true, true], _G2048) ? 

Answer 1

因爲這個經常出現，這裏有一個具體化的真理價值的實現不依賴於否定爲失敗：

eval(atom(true),true). 
eval(atom(false),false). 
eval(and(A,B),true) :- 
    eval(A,true), 
    eval(B,true). 
eval(and(A,_B),false) :- 
    eval(A,false). 
eval(and(_A,B),false) :- 
    eval(B,false). 
eval(neg(A),false) :- 
    eval(A,true). 
eval(neg(A),true) :- 
    eval(A,false). 
eval(or(A,B),C) :- 
    eval(neg(and(neg(A),neg(B))),C). 
eval(impl(A,B),C) :- 
    eval(neg(and(A,neg(B))),C). 

它使輸出：

?- eval(or(atom(A),and(atom(A),atom(B))), T). 
A = T, T = false ; 
A = B, B = T, T = false ; 
A = T, T = true ; 
A = B, B = T, T = true ; 
false. 

有intentio最終沒有優化。爲了做得更好，我建議使用語義tableaux或分辨率來代替真值表。