home *** CD-ROM | disk | FTP | other *** search
/ ftp.cs.yorku.ca 2015 / ftp.cs.yorku.ca.tar / ftp.cs.yorku.ca / pub / peter / SVT / wang.prolog < prev   
Text File  |  2002-07-29  |  4KB  |  125 lines
  1. /******************************************************************************
  2. *
  3. *  Checks a file of propositions and reports for each proposition
  4. *  whether it is a tautology.  Each proposition is a term constructed from
  5. *  'not', 'and', 'or', 'xor', 'implies', 'iff', 'true', 'false', 
  6. *  and Prolog terms.  Each term must end in '.'.
  7. *
  8. *  The predicate tautology(Term) succeeds if Term represents a tautology. It
  9. *  uses Wang's algorithm for proving theorems in the propositional calculus
  10. *  using sequents.
  11. *
  12. ******************************************************************************/
  13. % Ver 1.0, P. H. Roosen-Runge, December 1990.
  14. % Ver 1.2, December 6, 1991:  modified for Quintus Prolog 3.1
  15. %     1.2.2  Feb. 23, 1992: input must be a ground term.
  16. %     1.3.1 July 5: rewritten for optimization, using Prolog's indexing
  17. %       on the principal functor of the first argument. Tracing removed.
  18. %     1.3.4 Dec. 21, 1998: relies on prolog.ini for path.
  19. %     1.4   Dec. 12, 1999: shows counter-example
  20. %     1.4.1 November 5, 2000: re-compiled with corrected operator precedence
  21. /*****************************************************************************/
  22. :- ensure_loaded([library(basics), library(sets)]).
  23. % path defined in prolog.ini
  24. :- ensure_loaded(lib('operators.prolog')). 
  25.  
  26. user_error_handler(_,_,_,_) :-  error('!! Something wrong.').
  27. error(X) :- write('!! '), write(X), nl.
  28. activate :- write('Version 1.4.1, November 5, 2000.'), nl,
  29.       propositions
  30.      ;
  31.       nl, error('Something wrong.'), halt.
  32.  
  33. propositions :- read(T),
  34.     (  T==end_of_file, halt
  35.      ; 
  36.             nl, write(T), nl,
  37.             \+ ground(T) -> nl, 
  38.                error('Prolog variable in input. Use lower-case or quote it.')
  39.      ; 
  40.         check(T)
  41.     ), 
  42.     propositions.
  43.  
  44. check(T) :- 
  45.                (tautology(T), nl, display('* Valid.'), nl, nl  
  46.               ;
  47.                 nl, display('* Not valid.')), nl, nl.
  48.  
  49. tautology(Term) :- !, sweepR(Term, []>>[], []>>[]).
  50.  
  51. checkAtoms(S, LAtoms>>RAtoms) :- 
  52.     ok(LAtoms, RAtoms), !
  53.     ;
  54.     S \== ([]>>[]) -> sweep(S, LAtoms>>RAtoms)
  55.     ; noLogical(LAtoms), noLogical(RAtoms),
  56.          showCounterExample(LAtoms, RAtoms),!, fail
  57.         ; fail. %  no counterexample for [true] >> [false], etc.
  58.  
  59. ok(LAtoms, RAtoms) :-
  60.     memberchk(false, LAtoms) ; memberchk(true, RAtoms)
  61.         ;
  62.         member(M, LAtoms), member(M, RAtoms).
  63.  
  64. noLogical([]).
  65. noLogical([First | Rest]) :- 
  66.      \+ logical(First),
  67.      noLogical(Rest).
  68.  
  69. logical(First) :- 
  70.         functor(First, true, 0) ; functor(First, false, 0) ;
  71.     functor(First, not, 1) ;
  72.     functor(First, F, 2), member(F, [and, or, iff, xor, implies]).
  73.     
  74. showCounterExample(Left, Right) :-
  75.     nl, write('Counterexample: '),
  76.     Left = [] ->
  77.              writeSet(Right), write(' is false.')
  78.     ;
  79.         Right = [] ->
  80.          writeSet(Left), write(' is true.')
  81.     ;
  82.     writeSet(Left), write(' is true and '),
  83.     writeSet(Right), write(' is false.').
  84.  
  85. writeSet([X]) :- write(X).
  86. writeSet(X) :- 
  87.     list_to_set(X, Set),
  88.     ( Set = [S] -> write(S)
  89.          ;
  90.           write('each of '), write(Set)
  91.         ).
  92.  
  93. sweep([P | Rest]>>R, Atoms) :- !, sweepL(P, Rest>>R, Atoms).
  94. sweep(L>>[P | Rest], Atoms) :- !, sweepR(P, L>>Rest, Atoms).
  95.  
  96. sweepR(not P, S, Atoms) :- !, sweepL(P, S, Atoms).
  97. sweepR(C1 or C2, L>> Rest, Atoms) :- !, sweepR(C1, L>>[C2 | Rest], Atoms).
  98. sweepR(C1 implies C2, L>>R, Atoms) :- 
  99.         !, sweepR(C2, [C1 | L]>>R, Atoms).        
  100. sweepR(C1 and C2, S, Atoms) :-
  101.         !, sweepR(C1, S, Atoms), !,
  102.         sweepR(C2, S, Atoms).
  103. sweepR(C1 iff C2, L>>R, Atoms) :-
  104.         !, sweepR(C2, [C1 | L]>>R, Atoms), !,
  105.                 sweepR(C1, [C2 | L]>>R, Atoms).
  106. sweepR(C1 xor C2, S, Atoms) :-  !, sweepL(C1 iff C2, S, Atoms).
  107. sweepR(P, S, LAtoms>>RAtoms) :- checkAtoms(S, LAtoms>>[P | RAtoms]).
  108.  
  109. sweepL(not P, S, Atoms) :- !, sweepR(P, S, Atoms).
  110. sweepL(C1 and C2,  Rest>>R, Atoms) :- !, sweepL(C1, [C2 | Rest] >> R, Atoms).
  111. sweepL(C1 or C2, S, Atoms) :-
  112.                 !, sweepL(C1, S, Atoms), !,
  113.                 sweepL(C2, S, Atoms).
  114. sweepL(C1 implies C2, S, Atoms) :-
  115.                 !, sweepR(C1, S, Atoms), !,
  116.                 sweepL(C2, S, Atoms).
  117. sweepL(C1 iff C2, Rest>>R, Atoms) :-
  118.         !, sweepL(C1 implies C2, [C2 implies C1 | Rest]>>R, Atoms).
  119. sweepL(C1 xor C2, S, Atoms) :-    !, sweepR(C1 iff C2, S, Atoms).
  120.     
  121. sweepL(P, S, LAtoms>>RAtoms) :- checkAtoms(S, [P | LAtoms]>>RAtoms).
  122.  
  123. :-save_program(wang, activate).
  124.  
  125.