home *** CD-ROM | disk | FTP | other *** search
/ ftp.cs.yorku.ca 2015 / ftp.cs.yorku.ca.tar / ftp.cs.yorku.ca / pub / peter / SVT / OpenProlog / wang.prolog < prev   
Text File  |  1999-04-04  |  4KB  |  142 lines
  1. /*
  2.   Wang's algorithm
  3.  
  4.   copyright P. H. Roosen-Runge, October 1990.
  5.  
  6.   Version 1.4,  April 1999, adapted for Open Prolog.
  7.  
  8.  
  9.    Examples:
  10. =====================
  11. go.
  12.  
  13. x>0 or not x>0.
  14.  
  15. * Valid.
  16.  
  17.  
  18. 0=0.
  19.  
  20. * Not valid.
  21.  
  22.  
  23. X implies true.
  24.  
  25. Prolog variable in input. Use lower-case or quote it
  26.                                      
  27. ====================                                                                      
  28.   Formulae should only contain non-logical ground terms (with lower-case letters for variables), the atoms 'true' and 'false', the operators 'not', 'and', 'or', 'xor', 'implies', 'iff' and parentheses. 
  29.  
  30. The predicate tautology(Term) succeeds if Term represents a tautology. It
  31. uses Wang's method of sequents to check Term.
  32.  
  33. */
  34.  
  35. go :- propositions.
  36.  
  37. propositions :- 
  38.    nl, nl,  read(T), nl, 
  39.    (
  40.     \+ ground(T) -> nl, 
  41.     write('Prolog variable in input. Use lower-case or quote it.')
  42.        ; 
  43.         check(T)
  44.       ), 
  45.       propositions.
  46.  
  47. check(T) :- 
  48.      (
  49.        tautology(T), 
  50.        nl, write('* Valid.')
  51.       ;
  52.        nl, write('* Not valid.')
  53.      ), nl.
  54.  
  55. tautology(Term) :- !, sweepR(Term, []>>[], []>>[]).
  56.  
  57. checkAtoms(S, LAtoms>>RAtoms) :- 
  58.         memberchk(false, LAtoms) ; memberchk(true, RAtoms)
  59.     ;
  60.         member(M, LAtoms), member(M, RAtoms)
  61.     ;
  62.         S \== ([]>>[]) -> sweep(S, LAtoms>>RAtoms).
  63.  
  64. sweep([P | Rest]>>R, Atoms) :- !, sweepL(P, Rest>>R, Atoms).
  65. sweep(L>>[P | Rest], Atoms) :- sweepR(P, L>>Rest, Atoms).
  66.  
  67. sweepR(not P, S, Atoms) :- sweepL(P, S, Atoms).
  68. sweepR(C1 or C2, L>> Rest, Atoms) :- sweepR(C1, L>>[C2 | Rest], Atoms).
  69. sweepR(C1 implies C2, L>>R, Atoms) :- sweepR(C2, [C1 | L]>>R, Atoms).        
  70. sweepR(C1 and C2, S, Atoms) :- sweepR(C1, S, Atoms), sweepR(C2, S, Atoms).
  71. sweepR(C1 iff C2, L>>R, Atoms) :-
  72.         sweepR(C2, [C1 | L]>>R, Atoms),
  73.   sweepR(C1, [C2 | L]>>R, Atoms).
  74. sweepR(C1 xor C2, S, Atoms) :-  sweepL(C1 iff C2, S, Atoms).
  75. sweepR(P, S, LAtoms>>RAtoms) :- checkAtoms(S, LAtoms>>[P | RAtoms]).
  76.  
  77. sweepL(not P, S, Atoms) :- sweepR(P, S, Atoms).
  78. sweepL(C1 and C2,  Rest>>R, Atoms) :- sweepL(C1, [C2 | Rest] >> R, Atoms).
  79. sweepL(C1 or C2, S, Atoms) :- sweepL(C1, S, Atoms), sweepL(C2, S, Atoms).
  80. sweepL(C1 implies C2, S, Atoms) :- sweepR(C1, S, Atoms), sweepL(C2, S, Atoms).
  81. sweepL(C1 iff C2, Rest>>R, Atoms) :- 
  82.    sweepL(C1 implies C2, [C2 implies C1 | Rest]>>R, Atoms).
  83. sweepL(C1 xor C2, S, Atoms) :-    sweepR(C1 iff C2, S, Atoms).
  84. sweepL(P, S, LAtoms>>RAtoms) :- checkAtoms(S, [P | LAtoms]>>RAtoms).
  85.  
  86. % Library stuff
  87.  
  88. % COMMON OPERATORS
  89. % revised February 17, 1999
  90.  
  91. % For consistency, operator declarations used by wang, taut, simp, symbex, and
  92. % quants are loaded from this file.
  93.  
  94. :-op(999,xfx, '!'). % used to separate condition from current function.
  95. :-op(995,xfx, '->>').  % simplification
  96. :-op(995,xfy,'>>').    % sequent 
  97. :-op(995,xfy, '::').  % separate parts of a quantified expression
  98. :-op(990, yfx, iff).  % Left-associative (yfx) for consistency with 
  99.                       % commutative arithmetic operators.
  100.  
  101. :-op(990,yfx,implies). % for consistency with iff
  102. :-op(980,yfx, [or, cor]).
  103. :-op(970,xfx,xor). % xor isn't associative.  force parenthesization.
  104. :-op(960,yfx,[and, cand]).
  105. :-op(950,fy,not).
  106. :-op(700,xfx,assigned).  % used in simplification. A safe 'is' operator.
  107. :-op(700,yfx,['<=','<', '>', '>=', '<>', '!=']). % was right-associative
  108. :-op(400, xfx, [div, mod]).
  109. :-op(200, xfy,'**').
  110.  
  111. /* Routines to substitute for QP basics library, and builtins */
  112.  
  113. arity(Term, N) :- functor(Term, _, N).
  114. functor(Term, F) :- functor(Term, F, _).
  115.  
  116. args(Term, A) :- Term =.. [_ | A].
  117.  
  118. ground(Term) :- nonvar(Term), Term =.. [_ | Args], groundList(Args).
  119.  
  120. groundList([]).
  121. groundList([Arg | Rest]) :- ground(Arg), groundList(Rest).
  122.  
  123. memberchk(X, [X|_]) :- !.
  124. memberchk(X, [_|Rest]) :- memberchk(X, Rest).
  125.  
  126. member(X, [X|_]).
  127. member(X, [_|Rest]) :- member(X, Rest).
  128.  
  129. :- 'system$alert'(
  130.         'Tautology checking with Wang╣s algorithm,
  131. Version 1.4, April 1999.
  132.  
  133. ⌐ P. H. Roosen-Runge, 1999','','','').
  134.  
  135.  
  136.  
  137.  
  138.  
  139.  
  140.  
  141.  
  142.