序言中的真实分裂 [英] truthtable split in prolog

问题描述

Hello stackoverflow community

so I am trying to compute this output

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  

however my code gives me error when I consult it

here is my code

    :- 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).

error when consulting

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

aswell as an error when i type a statement

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) ? 

解决方案

Since this comes up so often, here an implementation with a reified truth value which does not rely on negation as failure:

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).

It gives the output:

?- 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.

There's intentionally no optimization. To do better, I'd propose using semantic tableaux or resolution instead of truth tables.

这篇关于序言中的真实分裂的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！