Interactive Logic Programs

      Solve Linear Diophantine Equations

    • Truth Tables NOTE: NOT WORKING PROPERLY
    • Propositional Connectives
    • Davis-Putnam Procedure
    • Parse Terms and Atomic Formulas
    • Unification Algorithm
    • Critical Pairs
    • Critical Pairs Theorem Proving
    • Knuth-Bendix Term Orderings
    • William McCune's Automated Theorem Prover
  • You can work with Truth Tables . NOTE: NOT WORKING PROPERLY

    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.

  • William McCune's Automated Theorem Provers.

    • These programs are among the best automated theorem provers. For example, Otter was used to give an affirmative answer to Robbins Conjecture regarding an equational basis for Boolean algebra.