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.

Circuit Verification

Software Correctness