TAUT : term -> thm

SYNOPSIS

Proves a propositional tautology.

DESCRIPTION

The call TAUT `t` where t is a propositional tautology, will prove it automatically and return |- t. A propositional tautology is a formula built up using the logical connectives `~', `/\', `\/', `==>' and `<=>' from terms that can be considered ``atomic'' that is logically valid whatever truth-values are assigned to the atomic formulas.

FAILURE CONDITIONS

Fails if t is not a propositional tautology.

EXAMPLE

Here is a simple and potentially useful tautology:

  # TAUT `a \/ b ==> c <=> (a ==> c) /\ (b ==> c)`;;
  val it : thm = |- a \/ b ==> c <=> (a ==> c) /\ (b ==> c)

and here is a more surprising one:

  # TAUT `(p ==> q) \/ (q ==> p)`;;
  val it : thm = |- (p ==> q) \/ (q ==> p)

Note that the ``atomic'' formulas need not just be variables:

  # TAUT `(x > 2 ==> y > 3) \/ (y < 3 ==> x > 2)`;;
  val it : thm = |- (x > 2 ==> y > 3) \/ (y < 3 ==> x > 2)

USES

Solving a tautologous goal completely by CONV_TAC TAUT, or generating a tautology to massage the goal into a more convenient equivalent form by REWRITE_TAC[TAUT `...`] or ONCE_REWRITE_TAC[TAUT `...`].

COMMENTS

The algorithm used is quite naive, and not efficient on large formulas. For more general first-order reasoning, with quantifier instantiation, use MESON-based methods.