ftp.cs.yorku.ca 2015/ftp.cs.yorku.ca.tar/ftp.cs.yorku.ca/pub/peter/SVT/GNU/wang.pl

Text File | 2002-12-05 | 6KB | 174 lines

/*******************************************************************************
*  Wang's Algorithm
* (c) P. H. Roosen-Runge, 2002.

*  Checks a file of propositions and reports for each proposition
*  whether it is a tautology.  Each proposition is a term constructed from
*  'not', 'and', 'or', 'xor', 'implies', 'iff', 'true', 'false',
*  and Prolog terms.  Each term must end in '.'.
*
*  The predicate tautology(Term) succeeds if Term represents a tautology. It
*  uses Wang's algorithm for proving theorems in the propositional calculus
*  using sequents.
*
******************************************************************************/
% Ver 1.0, P. H. Roosen-Runge, December 1990.
% Ver 1.2, December 6, 1991:  modified for Quintus Prolog 3.1
%     1.2.2  Feb. 23, 1992: input must be a ground term.
%     1.3.1 July 5: rewritten for optimization, using Prolog's indexing
%       on the principal functor of the first argument. Tracing removed.
%     1.4   Dec. 12, 1999: shows counter-example

%     1.4GNU November 4, 2002: Gnu Prolog version
%     1.41GNU Dec. 5: fixed counter-example printing
/*****************************************************************************/

:-op(995,xfy,'>>').    % sequent
:-op(990, yfx, iff).  % Left-associative (yfx) for consistency with
                      % commutative arithmetic operators.

:-op(990,yfx,implies). % for consistency with iff
:-op(980,yfx, [or, cor]).
:-op(970,xfx,xor). % xor isn't associative.  force parenthesization.
:-op(960,yfx,[and, cand]).
:-op(950,fy,not).
:-op(700,yfx,['<=','<', '>','=>', '>=', '<>', '!=']). % was right-associative
:-op(400, xfx, [div, mod]).
:-op(200, xfy,'**').
:-op(200, xf, '!').

:- initialization(activate).   % gprolog

error(X) :- write('!! '), write(X), nl.
activate :-
      set_linedit_prompt('|:'),
      write('wang: version 1.41GNU, December 5, 2002.'), nl,
      propositions
     ;
      nl, error('Something wrong.'), halt.

propositions :- read(T),
    (  T==end_of_file, halt
     ;
            nl, write(T), nl,
       \+ ground(T) -> nl,  % defined below; not in gprolog.
               error('Prolog variable in input. Use lower-case or quote it.')
     ;
        check(T)
    ),
    propositions.

check(T) :-
        (
         tautology(T), nl, display('* Valid.'), nl, nl
        ;
        nl, display('* Not valid.')
        ),
        nl, nl.

tautology(Term) :- (!), sweepR(Term, ([]>>[]), ([]>>[])).

checkAtoms(S, LAtoms>>RAtoms) :-
    ok(LAtoms, RAtoms), (!)  % gprolog parser problem?
    ;
    S \== ([]>>[]) -> sweep(S, LAtoms>>RAtoms)
    ;
        noLogical(LAtoms), noLogical(RAtoms),
         showCounterExample(LAtoms, RAtoms),(!), fail
        ;
        RAtoms = [false], noLogical(LAtoms),
        nl, write('Counterexample: '),
        writeSet(LAtoms), write(' is true.'), (!), fail
        ;
        LAtoms = [true], noLogical(RAtoms),
        nl, write('Counterexample: '),
        writeSet(RAtoms), write(' is false.'), (!), fail
        ;
        fail. %  no counterexample for [true] >> [false], etc.

ok(LAtoms, RAtoms) :-
    memberchk(false, LAtoms) ; memberchk(true, RAtoms)
        ;
        member(M, LAtoms), member(M, RAtoms).


noLogical([]).
noLogical([First | Rest]) :-
     \+ logical(First),
     noLogical(Rest).

logical(First) :-
        functor(First, true, 0) ; functor(First, false, 0) ;
    functor(First, not, 1) ;
    functor(First, F, 2), member(F, [and, or, iff, xor, implies]).

showCounterExample(Left, Right) :-
    nl, write('Counterexample: '),
    Left = [] -> writeSet(Right), write(' is false.')
    ;
        Right = [] -> writeSet(Left), write(' is true.')
        ;
    writeSet(Left), write(' is true and '),
    writeSet(Right), write(' is false.').

writeSet([X]) :- write(X).
writeSet(X) :-
    list_to_set(X, Set),
       (
        Set = [Single], write(Single)
        ;
    write('each of '), write(Set)
       ).

sweep([P | Rest]>>R, Atoms) :- (!), sweepL(P, Rest>>R, Atoms).
sweep(L>>[P | Rest], Atoms) :- (!), sweepR(P, L>>Rest, Atoms).

sweepR(not P, S, Atoms) :- (!), sweepL(P, S, Atoms).
sweepR(C1 or C2, L>> Rest, Atoms) :- (!), sweepR(C1, L>>[C2 | Rest], Atoms).
sweepR(C1 implies C2, L>>R, Atoms) :-
        (!), sweepR(C2, [C1 | L]>>R, Atoms).
sweepR(C1 and C2, S, Atoms) :-
        (!), sweepR(C1, S, Atoms), (!),
        sweepR(C2, S, Atoms).
sweepR(C1 iff C2, L>>R, Atoms) :-
        (!), sweepR(C2, [C1 | L]>>R, Atoms), (!),
                sweepR(C1, [C2 | L]>>R, Atoms).
sweepR(C1 xor C2, S, Atoms) :-  (!), sweepL(C1 iff C2, S, Atoms).
sweepR(P, S, LAtoms>>RAtoms) :- checkAtoms(S, LAtoms>>[P | RAtoms]).

sweepL(not P, S, Atoms) :- (!), sweepR(P, S, Atoms).
sweepL(C1 and C2,  Rest>>R, Atoms) :- (!), sweepL(C1, [C2 | Rest] >> R, Atoms).
sweepL(C1 or C2, S, Atoms) :-
                (!), sweepL(C1, S, Atoms), (!), sweepL(C2, S, Atoms).
sweepL(C1 implies C2, S, Atoms) :-
                (!), sweepR(C1, S, Atoms), (!), sweepL(C2, S, Atoms).
sweepL(C1 iff C2, Rest>>R, Atoms) :-
        (!), sweepL(C1 implies C2, [C2 implies C1 | Rest]>>R, Atoms).
sweepL(C1 xor C2, S, Atoms) :-    (!), sweepR(C1 iff C2, S, Atoms).

sweepL(P, S, LAtoms>>RAtoms) :- checkAtoms(S, [P | LAtoms]>>RAtoms).

ground(T) :-
    nonvar(T),
   (
     functor(T, _, 0)
    ;
     T =.. [_ | Args], grounds(Args)
   ).

grounds([T]) :- ground(T).
grounds([H | T]) :- ground(H), grounds(T).

%   list_to_set(+List, ?Set)

%   Authors: Lawrence Byrd + Richard A. O'Keefe
%   Updated: 19 Jan 1994

list_to_set([], []).
list_to_set([Head|Tail], Set) :-
    memberchk(Head, Tail),
    (!),
    list_to_set(Tail, Set).
list_to_set([Head|Tail], [Head|Set]) :-
    list_to_set(Tail, Set).