COMP 426 Automated Reasoning
Projects

We will form groups of 2 or 3 students to design and implement an inverse theorem provers for first-order intuitionistic logic. In each week (Thursday to Thursday) there should be a well-defined plan for the coming week and a result to be reported at the end of the week. The plan for the next week and the report for the previous week should be e-mailed to the instructor prior to Thursday's lecture. Each week someone else should write and send the plan and report.

• The plan should be about 1-2 pages, and be organized according to all tasks relevant for that week.
• The report should be about 2-3 pages and summarize the accomplishments or failures with respect to the various planned tasks.
• The code should be tagged in the CVS repository (week1, week2, etc.) and be available for inspection. It should compile and run to the extent described in the report.

Theorem proving frame

In this project, you should concentrate on developing the proof search and proof checking procedure for a first-order theorem prover. therefore, we will provide a code frame which will facilitate the building of a theorem prover. You can find the code here. The code provided will contain:

Interface and Parsing

We use the first-order formula (FOF) syntax of the TPTP (Thousands of Problems for Theorem Provers) library. The theorem proving code frame provided already contains a parser and an interface for reading files which may contain a theory and a given conjecture.

Test-suite

We have converted many problems from the TPTP (Thousands of Problems for Theorem Provers) library. Since the TPTP library contains classical theorems, only a subset of the given problems are valid in the intuitionistic logic. All Horn problems in the TPTP library should be valid problems. You are encouraged to add and translate your own problems. In particular, it would be great to build up a section on intuitionistic theorems in the TPTP library.

Timing

To help you evaluate your prover and the different techniques you are going to implement, we have provided a basic module for timing.

Validation

Besides the usual testing, our theorem prover will produce proof terms which must be independently verifiable by a proof checker. We have already provided a bi-directional checker, and a pretty printer which will print the found proof in natural deduction style.

Methods

Each group should implement a prover based on forward search. Below are some possible intermediate goals for the prover. You can create your own milestones, but you should send me a detailled timetable.

Forward Search -- Possible timetable

• Oct 28 - Nov 4: Inverse method prover for intuitionistic propositional logic
• Nov 4 - Nov 11: Exploiting focusing
• Nov 11 - Nov 18: A first-order intuitionistic inverse method prover.
• Nov 18 - Nov 25: Optimizations: indexing, selection, ordering, types, constraints etc.
• Nov 25 - Nov 30: Final report with a discussion of validation and testing

Tasks

For each prover or group a number of tasks arise. You should try to rotate between tasks so everyone in the group gets some exposure to various aspects of the prover.

Inference Engine

This is the main task in the project. The search engine includes the basic inference mechanism, termination criteria, focusing strategies and (in the first order case) unification.

Evaluation and Examples Suites

Various choices, heuristic, or stages in the prover should be evaluated against each other. This should employ some problems as gleaned from the TPTP, the test-suite provided, as well as some of your own theories. Some sources:

• Horn theories (possibly syntactically transformed).
• Classical theories, using double-negation or similar translations.
• Automatically generated test problems.
• Example suites from other intuitionistic provers.
• Constructive geometry (Jan von Plato).
• Qualitative spatial reasoning in intuitionistic logic (e.g., Anthony Cohn or Brandon Bennett).
• Constructive set theory.
• Other constructive theories in Coq, Nuprl or related systems (but beware the pervasive use of induction).

Documentation and Summary

Besides the weekly plan and summary, there should be sufficient documentation of the code to make it readable. Also, there should be a final summary paper describing all aspects of the project. This includes the inference engine, the validation techniques, the sample suites and the empirical results.

References

Besides the lecture notes, here are further references that may be useful to each kind of prover.

Forward Search (Inverse Method and Resolution)

These are only a few pointers, including one implementation home page. Further references can be found in the papers below and among the handouts.

Implementations

• Gandalf by Tanel Tammet (see [T96]), based on the inverse method (forward).

[ Home | Schedule | Assignments | Handouts | Software | Overview ]

bp@cs.mcgill.ca
Brigitte Pientka