1\DOC PTAUT_TAC 2 3\TYPE {PTAUT_TAC : tactic} 4 5\SYNOPSIS 6Tautology checker. Proves propositional goals. 7 8\LIBRARY taut 9 10\DESCRIBE 11Given a goal with a conclusion that contains only Boolean constants, 12Boolean-valued variables, Boolean equalities, implications, conjunctions, 13disjunctions, negations and Boolean-valued conditionals, this tactic will 14prove the goal if it is valid. If all the variables in the conclusion are 15universally quantified, this tactic will also reduce an invalid goal to false. 16 17\FAILURE 18Fails if the conclusion of the goal is not of the form 19{!x1 ... xn. f[x1,...,xn]} where {f[x1,...,xn]} is a propositional formula 20(except that the variables do not have to be universally quantified if the 21goal is valid). 22 23\SEEALSO 24tautLib.PTAUT_CONV, tautLib.PTAUT_PROVE, tautLib.TAUT_TAC. 25 26\ENDDOC 27