tautLib.PTAUT

STRUCTURE

SYNOPSIS

Tautology checker. Proves closed propositional formulae true or false.

LIBRARY

taut

DESCRIPTION

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

PTAUT_PROVE, PTAUT_TAC, TAUT_CONV