----------------------------------------------------------------------
PTAUT_CONV                                                   (tautLib)
----------------------------------------------------------------------
PTAUT_CONV : conv

SYNOPSIS
Tautology checker. Proves closed propositional formulae true or false.

LIBRARY
taut

DESCRIBE
Given a term of the form {"!x1 ... xn. t"} where {t} contains only Boolean
constants, Boolean-valued variables, Boolean equalities, implications,
conjunctions, disjunctions, negations and Boolean-valued conditionals, and
all the variables in {t} appear in {x1 ... xn}, the conversion {PTAUT_CONV}
proves the term to be either true or false, that is, one of the following
theorems is returned:

   |- (!x1 ... xn. t) = T
   |- (!x1 ... xn. t) = F

This conversion also accepts propositional terms that are not fully
universally quantified. However, for such a term, the conversion will only
succeed if the term is valid.

FAILURE
Fails if the term is not of the form {"!x1 ... xn. f[x1,...,xn]"} where
{f[x1,...,xn]} is a propositional formula (except that the variables do not
have to be universally quantified if the term is valid).

EXAMPLE

#PTAUT_CONV ``!x y z w. (((x \/ ~y) ==> z) /\ (z ==> ~w) /\ w) ==> y``;
|- (!x y z w. (x \/ ~y ==> z) /\ (z ==> ~w) /\ w ==> y) = T

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

#PTAUT_CONV ``!x. x = T``;
|- (!x. x = T) = F

#PTAUT_CONV ``x = T``;
Uncaught exception:
HOL_ERR


SEEALSO
tautLib.PTAUT_PROVE, tautLib.PTAUT_TAC, tautLib.TAUT_CONV.

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