Paul Haroun

PhD student

McGill University

School of Computer Science



PhD Thesis The application of augmented data structures, hashing and heuristics in automated theorem proving
Supervisor Professor Monty Newborn


Brief description of our work

The applications of theorem proving and automated reasoning in general in many domains is becoming more popular due to the advancements in hardware. However, no matter how fast computers are and no matter how much memory they contain, improvements in the design and implementation of an automated theorem prover are still the major impacts on its  performance. We are always trying to find new methods, strategies and data structures to improve the search process whether by reducing the size of the search space or by reducing the amount of repetitive computations. 

Based on ideas from the theorem prover THEO developed by Professor Newborn, we are developing a new theorem prover which is an experimental system to demonstrate that certain major computations can be avoided by keeping track of the minor changes in linear and semi-linear resolution based theorem provers. We have also discovered from this process and through experimental data  that certain heuristics can be used to reduce the search space.  The process is quite simple yet can be applied to many theorem provers without affecting their strategies. We are trying to prove which strategies will maintain their degree of completeness and soundness if they adopt this process. Also the degree of complexity for the integration of such process is an issue we are studying. There are several optimizations that can be made to improve the process itself but this is left for future work.  

The program, CARINE, that  we are developing, is a first order predicate automated theorem prover which is based on an iteratively deepening depth first search algorithm. Proofs generated by CARINE are semi-linear. The inference rules implemented so far are binary resolution and binary factoring. Strategies include pure literal deletion, unit clause resolutions, memoization, delayed clause construction, time slicing, and extended depth search. Heuristics are deployed at different stages to restrict the search space.




Automated Reasoning and Theorem Proving Links

Advances in Modal Logic
Association for Automated Reasoning
The CADE ATP System Competition
Logic Animations
Bliksem: Resolution Based Theorem Prover
Isabelle: Generic Theorem Proving Environment
Otter: An Automated Deduction System
SPASS: An Automated Theorem Prover for First-Order Logic with Equality
Vampire - A Theorem Prover for First-Order Classical Logic
Induction Theorem Proving Systems




Some Applications of Theorem Proving

Circuit Verification

ACL2, successor to Nqtm (Boyer-Moore Theorem Prover), used at AMD to formally verify floating point units
used by Moore et al. to check the proof of correctness of the Kernel of the AMD 5k86 floating point division algorithm
used to verify the RTL (logical operations on bit vectors) of the K7 Floating Point Unit

Software Correctness

Software Correctness and Safety Research Laboratory
Privacy Properties of Data Mining Software
Feature Interaction
Protocol Verification
VerifiCard Project




Thank you for your visit


updated on 16/07/2003 at 12:28:16 PM