PTAUT_PROVE : term -> thm
STRUCTURE
tautLib
SYNOPSIS
Tautology checker. Proves propositional formulae.
LIBRARY
taut
DESCRIPTION
Given a term that contains only Boolean constants, Boolean-valued variables, Boolean equalities, implications, conjunctions, disjunctions, negations and Boolean-valued conditionals, PTAUT_PROVE returns the term as a theorem if it is valid. The variables in the term may be universally quantified.
FAILURE
Fails if the term is not a valid propositional formula.
EXAMPLE
#PTAUT_PROVE ``!x y z w. (((x \/ ~y) ==> z) /\ (z ==> ~w) /\ w) ==> y``;
|- !x y z w. (x \/ ~y ==> z) /\ (z ==> ~w) /\ w ==> y

#PTAUT_PROVE ``(((x \/ ~y) ==> z) /\ (z ==> ~w) /\ w) ==> y``;
|- (x \/ ~y ==> z) /\ (z ==> ~w) /\ w ==> y

#PTAUT_PROVE ``!x. x = T``;
Uncaught exception:
HOL_ERR

#PTAUT_PROVE ``x = T``;
Uncaught exception:
HOL_ERR
SEEALSO
PTAUT_CONV, PTAUT_TAC, TAUT_PROVE
HOL  Trindemossen-1