This renewal project will continue the investigation of the Model Elimination (ME) procedure. The ME procedure, a linear input proof procedure, has received recent attention for several reasons, including the ability to use the elegant Prolog implementation architectures. Previous work has demonstrated by implementation that ME has an advantage over other uniform provers on an interesting set of hard problems. New investigation will attempt to overcome the most severe handicap of the ME procedure, no use of intermediate results, without destroying the speed advantage ME enjoys. For example, the optional nature of lemma use for ME invites highly selective mechanisms for Lemma retention. An alternate approach allows low selectivity but not as much possibility of high gains. Work will also continue on the development of sequential, parallel and distributed implementations of ME.
