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