TAUT_CONV : conv
STRUCTURE
tautLib
SYNOPSIS
Tautology checker. Proves instances of propositional formulae.
LIBRARY
taut
DESCRIPTION
Given an instance t of a valid propositional formula, TAUT_CONV proves the theorem |- t = T. A propositional formula is a term containing only Boolean constants, Boolean-valued variables, Boolean equalities, implications, conjunctions, disjunctions, negations and Boolean-valued conditionals. An instance of a formula is the formula with one or more of the variables replaced by terms of the same type. The conversion accepts terms with or without universal quantifiers for the variables.
FAILURE
Fails if the term is not an instance of a propositional formula or if the instance is not a valid formula.
EXAMPLE
#TAUT_CONV
# ``!x n y. ((((n = 1) \/ ~x) ==> y) /\ (y ==> ~(n < 0)) /\ (n < 0)) ==> x``;
|- (!x n y. ((n = 1) \/ ~x ==> y) /\ (y ==> ~n < 0) /\ n < 0 ==> x) = T

#TAUT_CONV ``((((n = 1) \/ ~x) ==> y) /\ (y ==> ~(n < 0)) /\ (n < 0)) ==> x``;
|- ((n = 1) \/ ~x ==> y) /\ (y ==> ~n < 0) /\ n < 0 ==> x = T

#TAUT_CONV ``!n. (n < 0) \/ (n = 0)``;
Uncaught exception:
HOL_ERR
SEEALSO
TAUT_PROVE, TAUT_TAC, PTAUT_CONV
HOL  Kananaskis-13