We show a few relativily short Prolog programs, that can all check a propositional formula for its general validity. In the end we compare them with full grown CLP(B) libraries available in various Prolog systems. We only make a small formula test.
Boole's Method
This method is based on taking the propositional formula f(x1,x2,..,xn), picking a variable x1 and then first trying substituting x1=0 and afterwards trying substituting x1=1. It is possible to realized this method by using Prolog logical variables and Prolog backtracking.
We do not need to define a lot of operators. We will use the predefined (+)/2 for disjunction and the predefined (*)/2 for conjunction. The (+)/2 is not the same as in Boole, he uses it for xor. What we define extra is negation:
:- op(300, fy, ~).
We do not need to write some code for substitution, since we will use instantiating a Prolog logical variable. We then define a predicate eval/2 which will do a partial evaluation of a propositional formula. The predicate makes use of simp/2 which does the reduction of a given logical connective, depending on whether some argument values are known or not.
eval(A, A) :- var(A), !.
eval(A+B, R) :- !, eval(A, X), eval(B, Y), simp(X+Y, R).
eval(A*B, R) :- !, eval(A, X), eval(B, Y), simp(X*Y, R).
eval(~A, R) :- !, eval(A, X), simp(~X, R).
eval(A, A).
simp(A, A) :- var(A), !.
simp(A+B, B) :- A == 0, !.
simp(A+B, A) :- B == 0, !.
simp(A+_, 1) :- A == 1, !.
simp(_+B, 1) :- B == 1, !.
simp(A*_, 0) :- A == 0, !.
simp(_*B, 0) :- B == 0, !.
simp(A*B, B) :- A == 1, !.
simp(A*B, A) :- B == 1, !.
simp(~A, 1) :- A == 0, !.
simp(~A, 0) :- A == 1, !.
simp(A, A).
The above code makes heavy use of cut (!)/0 to only apply the first match of a rule. Also it makes heavy use of var/1 to detect Prolog logical variables, and (==)/2 to check term identity, so that a variable is not prematurely instantiated. The main loop falsify/1 does the Prolog logical variable instantiation.
falsify(A) :- eval(A, B), term_variables(B, L), falsify(B, L).
falsify(0, _) :- !.
falsify(A, [0|_]) :- falsify(A), !.
falsify(A, [1|_]) :- falsify(A).
Here is an example run in any of your favorite ISO Prolog:
?- falsify(A+ ~A).
No /* Tautology */
?- falsify(A+ ~B).
A = 0,
B = 1 /* Counter Example */
Beth's Method
Beth's method takes another approach. It was describe by Evert W. Beth in his booklet Formal Methods from 1961. But we might also name it after Lewis Carol, the author of Alice in Wonderland, since post mortem notes about a method of trees was found.
Our code simplifies the reduction, in that we use a predicate falsify/1 for the False column und sat/1 for the True column. We do not reduce a False and True column at the same time. To reach closure of the semantic tableaux, we instantiate Prolog logical variables and let backtracking play through splitting reductions.
falsify(A) :- var(A), !, A = 0.
falsify(0).
falsify(A+B) :- falsify(A), falsify(B).
falsify(A*B) :- falsify(A); falsify(B).
falsify(~A) :- sat(A).
sat(A) :- var(A), !, A = 1.
sat(1).
sat(A+B) :- sat(A); sat(B).
sat(A*B) :- sat(A), sat(B).
sat(~A) :- falsify(A).
Again here is an example run in any of your favorite ISO Prolog:
?- falsify(A+ ~A).
No /* Tautology */
?- falsify(A+ ~B).
A = 0,
B = 1 /* Counter Example */
Maslov's Method
Maslov's method, unlike Boole's method and Beth's method, is not a model finder. In the propositional case, it will not output some valuation. Maslov's method can be seen as derived from Gentzen two-sided sequents, in that it only uses one-sided sequent, but signed formulas.
Maslov's method was proposed in Soviet Mathematical Doklady in 1964. A distinct mark is that the conjunction is additive, avoiding a split non-determinism, and that the disjunction is multiplicative, avoiding again non-determinism. The only choice is which non-literal to next reduce.
Since we reduce as long as there are non-literals, the identity rule (I) is actually realized with a prime formula and not with a formula. Because of inversion theorems, already found in Gentzen, its irrelevant which non-literal is chosen, so the method is complete for propositonal logic.
prove(L) :- select(A, L, R), \+ literal(A), !,
prove(A, R).
prove(L) :- select(A, L, R), var(A),
member(B, R), B == ~A, !.
prove(A+B, L) :- !, prove([A, B|L]).
prove(A*B, L) :- !, prove([A|L]), prove([B|L]).
prove(~ (A+B), L) :- !, prove([~A|L]), prove([~B|L]).
prove(~ (A*B), L) :- !, prove([~A, ~B|L]).
prove(~ ~A, L) :- prove([A|L]).
literal(A) :- var(A), !.
literal(~A) :- var(A).
Since its not a model finder, but a deductive method there is no predicate falsify/1. Instead the main predicate is prove/1 and we don't find the instantiation of Prolog logical variables, that again play the role of propositional variables. We can define falsify/1 as follows:
falsify(A) :- \+ prove([A]).
Once again here is an example run in any of your favorite ISO Prolog:
?- falsify(A+ ~A).
No /* Tautology */
?- falsify(A+ ~B).
Yes /* Not-Tautology */
The Comparison
As test cases we first used some 6 propositional logic non-tautologies from Fallacy Files, so as to see whether the various methods can indeed falsify formulas. We then did a benchmark with 193 propositional logic tautologies from Principia. We executed the test 1000 times and measured in milliseconds:
That the CLP(B) libraries will not fare so well, was to expect. They are made for checking sat(F1), .., sat(Fn) instead of sat(F1*..*Fn). Nevertheless their sat/1 could be directly used, since their internally used normal form usually gives the result immediately without labeling/1. We used SWI-Prolog 8.3.6 and Jekejeke Prolog 1.4.5 for testing.
Open Source: 193 Tautologies Principia
https://gist.github.com/jburse/4ab909be4406b0c960494c692fc7a37f#file-principia-pl
Open Source: CLP(B) Solver Stub
https://gist.github.com/jburse/4ab909be4406b0c960494c692fc7a37f#file-solver-pl