----------------------------------------------------------------------
PTAUT_PROVE                                                  (tautLib)
----------------------------------------------------------------------
PTAUT_PROVE : term -> thm

SYNOPSIS
Tautology checker. Proves propositional formulae.

LIBRARY
taut

DESCRIBE
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
tautLib.PTAUT_CONV, tautLib.PTAUT_TAC, tautLib.TAUT_PROVE.

----------------------------------------------------------------------