1\DOC TAUT_CONV 2 3\TYPE {TAUT_CONV : conv} 4 5\SYNOPSIS 6Tautology checker. Proves instances of propositional formulae. 7 8\LIBRARY taut 9 10\DESCRIBE 11Given an instance {t} of a valid propositional formula, {TAUT_CONV} 12proves the theorem {|- t = T}. A propositional formula is a term 13containing only Boolean constants, Boolean-valued variables, Boolean 14equalities, implications, conjunctions, disjunctions, negations and 15Boolean-valued conditionals. An instance of a formula is the formula 16with one or more of the variables replaced by terms of the same 17type. The conversion accepts terms with or without universal 18quantifiers for the variables. 19 20\FAILURE 21Fails if the term is not an instance of a propositional formula or if the 22instance is not a valid formula. 23 24\EXAMPLE 25{ 26#TAUT_CONV 27# ``!x n y. ((((n = 1) \/ ~x) ==> y) /\ (y ==> ~(n < 0)) /\ (n < 0)) ==> x``; 28|- (!x n y. ((n = 1) \/ ~x ==> y) /\ (y ==> ~n < 0) /\ n < 0 ==> x) = T 29 30#TAUT_CONV ``((((n = 1) \/ ~x) ==> y) /\ (y ==> ~(n < 0)) /\ (n < 0)) ==> x``; 31|- ((n = 1) \/ ~x ==> y) /\ (y ==> ~n < 0) /\ n < 0 ==> x = T 32 33#TAUT_CONV ``!n. (n < 0) \/ (n = 0)``; 34Uncaught exception: 35HOL_ERR 36} 37 38\SEEALSO 39tautLib.TAUT_PROVE, tautLib.TAUT_TAC, tautLib.PTAUT_CONV. 40 41\ENDDOC 42