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:
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
,