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