# Interactive Logic Programs

• You can work with Truth Tables .

This program allows you to select 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, "not", and the 16 binary connectives, and then to find which connectives can be expressed in terms of them. (See Sec 2.5 of LMCS.)

• You can work with the Davis-Putnam procedure.

This program allows you to select up to 10 clauses and have Thoralf apply the Davis-Putnam procedure 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.

This program allows you select two terms, 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 s1 --> t1 and s2 --> t2.

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

• You can experience the power of Critical Pairs Theorem Proving on equations of the form t = x.

This primitive program allows you to input a term t in prefix form and to try to automatically prove that t = x implies u = v. You may be surprised at how "clever" it can be.

There are two output formats: answer only, and detailed.

• Your are given a Knuth-Bendix Ordering and you can check the ordering that it establishes on your selected list of terms.

There are two output formats: answer only, and detailed.

• Test drive William McCune's online Automated Theorem Prover.

• This program allows you to choose a number of possible equational
premisses and conclusions and request a real time proof or refutation from the famous full range automated theorem prover Otter.