1\DOC TAUT_TAC 2 3\TYPE {TAUT_TAC : tactic} 4 5\SYNOPSIS 6Tautology checker. Proves propositional goals (and instances of them). 7 8\LIBRARY taut 9 10\DESCRIBE 11Given a goal that is an instance of a propositional formula, this tactic will 12prove the goal provided it is valid. 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 with one 16or more of the variables replaced by terms of the same type. The tactic 17accepts goals with or without universal quantifiers for the variables. 18 19\FAILURE 20Fails if the conclusion of the goal is not an instance of a propositional 21formula or if the instance is not a valid formula. 22 23\SEEALSO 24tautLib.TAUT_CONV, tautLib.TAUT_PROVE, tautLib.PTAUT_TAC. 25 26\ENDDOC 27