CanProve , Propositional logic theorem prover

Propositional logic theorem prover


CanProve(proposition)

Calling Sequence:
CanProve(proposition)
Parameters:
proposition - a logical proposition
Description:
Yacas has a small built-in propositional logic theorem prover. It can be invoked with a call to CanProve.
An example of a proposition is 'if a implies b and b implies c then a implies c'. Yacas supports the following operators

~ negation, read as 'not'
& conjunction, read as 'and'
| disjunction, read as 'or'
=> implication, read as 'implies'
So the above mentioned proposition would be represented by
( (a=>b)&(b=>c) ) => (a=>c)
Yacas can prove that is correct by applying CanProve to it:
In> CanProve(( (a=>b)&(b=>c) ) => (a=>c))
Out> True;
It does this the following way: in order to prove proposition p, it suffices to prove that ~p is false. It continues to simplify ~p using the rules

~ (~x)      --> x        eliminate double negation
x=>y        --> ~x | y   eliminate implication
~(x&y)      --> ~x | ~y  De Morgan's law
~(x | y)    --> ~x & ~y  De Morgan's law
(x & y) | z --> (x|z)&(y|z)  Distribution
x | (y & z) --> (x|y)&(x|z)  Distribution
And the obvious other rules: 'True|x --> True' etc. The above rules will translate the proposition into a form
(p1 | p2 | ...) & (q1 | q2 | ...) &...
If any of the clauses is false, the entire expression will be false. In the next step, clauses are scanned for situations of the form:
(p|Y) & (~p|Z) --> (Y|Z)
If this combination (Y|Z) is empty, it is false, and thus the entire proposition is false.

As a last step, the algorithm negates the result again. This has the added advantage of simplifying the expression further.

Examples:
In> CanProve(a | ~a)         
Out> True;
In> CanProve(True | a)       
Out> True;
In> CanProve(False | a)      
Out> a;
In> CanProve(a & ~a)         
Out> False;
In> CanProve(a |b|(a&b))     
Out> a|b;

See Also:
True , False ,