Tautology Checker, based on HOW TO SOLVE IT IN PROLOG, p. 68.
copyright P. H. Roosen-Runge, October 1990.
Version 2.5, April 1999, adapted for Open Prolog.
Example:
=====================
formulae. % input to top-level prompt.
P or not P.
A or not A % variables are renamed
* Valid.
P or Q implies P and Q.
A or B implies A and B
* Not valid.
* Counter-example: true or false implies true and false
====================
Formulae should only contain upper-case letters for variables, the atoms 'true' and 'false', the operators 'not', 'and', 'or', 'xor', 'implies', 'iff' and parentheses. (The operators are listed here in order of descending precedence.)
*/
:-op(990, yfx, iff). % left-associative for consistency with
% commutative arithmetic operators.
:-op(990,yfx,implies). % for consistency with iff
:-op(980,yfx, or).
:-op(970,xfx,xor). % xor isn't associative. force parenthesization.
:-op(960,yfx, and).
:-op(950,fy,not).
formulae :- read(T), theorem(T), formulae.
theorem(T) :-
nl, nl, prettyPrint(T), nl,
(
false(T), write('* Not valid.'), nl, write('* Counter-example: '), prettyPrint(T), !
;
write('* Valid.')
),
nl.
% logic rules
false('false').
false(not 'true') :-!.
false( P iff Q) :- false( (P implies Q) and (Q implies P)).