Artificial Intelligence

Project on Automated Proof

Draft Project Due: Monday, March 2 (written version only)
Final Project Due: Wednesday, March 4 (both written and e-mail copies)


Introduction

Chapter 3 presents several elements of an automated theorem-prover: As noted in the text, Theorem is based on the propositional calculus, while match, unify, disagreement supply critical elements to extend Theorem to the predicate calculus.

Chapter 4 suggests how search strategies can help drive applications, such as theorem proving.

Project Overview

In this project, you are to write a theorem-prover for expressions in the predicate calculus. Theorems may be written in either of two forms:
  1. Theorems may be written as a sequence of Horn clauses in the predicate calculus, or
  2. Theorems may be written as axioms in conjunctive normal form, with the theorem's conclusion negated.
In the first case, proof proceeds by goal reduction (with backward chaining); in the second case, proof proceeds by resolution and unification until a contradiction is obtained.

In this project, you are to write a theorem prover for one of these approaches. With either option, procedure Theorem should retain the same interface as the procedure in the text. Thus, Theorem will have two parameters: a desired conclusion and a list of rules or axioms.

Project Details

  1. If you choose to extend procedure Theorem in the book, your work should include the following:
    1. Allow recursive axioms (exercise 3.6),
    2. Extend Theorem to expressions in the predicate calculus (code for exercise 3.12),
    3. Reimplement Theorem to utilize a generic depth-first search (exercise 4.3).

      Altogether, this approach should yield a search-based procedure Theorem that will prove theorems based on (possibly-recursive) Horn clauses. If the result does not follow logically from the axioms, the theorem should report that fact.

      If desired (for extra credit), procedure Theorem might print out the steps involved in the proof.

    4. If you choose to write a theorem prover, based on axioms in conjunctive normal form, you should base a solution on the following:
      1. assume axioms are given in conjunctive normal form according to the syntax,
        • an axiom has the form (and B1 B2 ... Bn)
        • where each Bi has the form symbol, (not symbol), or (or C1 C2 ... Cm)
        • and where each symbol or Cj may be a free symbol or a constant symbol (const symbol) or a skolemization function (func symbol variable-parameters)
      2. assume the conclusion is given in positive form (so it will have to be negated before proof can begin).
      3. assume skolemization has already been performed for the given axioms and the conclusion.

      In your work, you may use any relevant parts of the programs in ~walker/261/labs/cnf.lsp which take any well-formed formula in the propositional calculus and place it in conjunctive normal form. (Only minor modifications would be needed to expand these procedures to include Skolemization constants and functions.)

      Altogether, this approach should yield a procedure Theorem that takes a conclusion and a list of axioms, such as your answers for the homework based on the resolution handout, and indicates either that the result is provable or that no proof is possible.

      If desired (for extra credit), procedure Theorem might print out the steps involved in the proof.


      Submitting Programs For This Project:

      A preliminary hard-copy version of your program should be turned in at class on Monday, March 2, and should include your code and either your test runs or a written status report on what remains to be done to complete your program.

      Final work for this project should be submitted in both written and electronic form. Written work should follow the format specified for Submitting Programs For This Course. An electronic copy of the final version of your program should be sent in ASCII format via e-mail to walker@math.grin.edu before class on Wednesday, March 4.


      This document is available on the World Wide Web as

      http://www.math.grin.edu/~walker/courses/261/proj-proof.html
      

      created February 22, 1998
      last revised February 22, 1998