Features Customized Input

Truth Tables
Propositional Connectives
Davis-Putnam procedure
Parse Terms and Atomic Formulas
Unification algorithm
Find the Critical Pairs
Knuth-Bendix Term Orderings
• William McCune's Automated Theorem Prover at the University of New Mexico

• You can work with Truth Tables

  This program allows you to enter up to 5 propositional formulas and

  • test any subset for satisfiability (see Sec. 2.7 of LMCS)
  • test any combination for giving a valid argument (see Sec. 2.7 of LMCS)
  • automatically construct a (combined) truth table for any
    combination of the formulas (see Sec 2.7 of LMCS).

  ---

• You can work with Propositional Connectives.

  This program allows you to select any of 0, 1, ¬, and the 16 binary connectives, and find which connectives can be expressed in terms of them, and how they can be expressed. (See Sec 2.5 of LMCS.)

  ---

• You can work with the Davis-Putnam procedure.

  This program allows you to input up to 15 propositional clauses, in up to 13 variables, and have the Davis-Putnam procedure applied to determine if the set of clauses is satisfiable. (See Sec. 2.10.4 of LMCS.

  ---

• You can Parse Terms and Atomic Formulas

  This program allows you to input a term or atomic formula in prefix form and have it parsed. (See Example 3.2.2, p. 140, and Example 4.3.3, p. 265, of LMCS.)

  ---

• You can apply the Unification algorithm

  to two Terms or Atomic Formulas.

  This program allows you to input terms or atomic formulas in prefix form and find their most general unifier, if it exists. (See Sec. 3.12.2 and Sec. 4.7.2 of LMCS).

  ---

• You can Find the Critical Pairs for two Term Rewrite Rules s₁ --> t₁ and s₂ --> t₂.

  This program allows you to input two rules with the terms in prefix form and to find all of their critical pairs. (See Sec. 3.13.4 of LMCS).

  ---

• Set up a Knuth-Bendix Term Ordering

  and check the ordering that it establishes on a chosen list of terms. (See Sec. 3.14.2.