Experiments with the ALPOC theorem prover
Loading...
Files
Date
1995
Journal Title
Journal ISSN
Volume Title
Publisher
Abstract
A system for selecting and preparing a batch of data files, and running a selected computer program with each data file is described. Another facility collects the experimental results from several different batches and summarizes the results in a tabular form.
A theorem prover, ALPOC, is implemented that combines Shostak's C-literal resolution steps with Stickel's PTTP compiler, and uses Spencer's Ordered Clause set restriction. A series of experiments is run that compares ALPOC with PTTP, using the batch system. The results are summarized and compared with Stickel's PTTP implemented in Prolog. The results show that ALPOC is slower than PTTP by a factor of at most 4, but frequently is much faster. On the problems where ALPOC is faster the number of extension steps in the ALPOC proof is less than the PTTP proof, which leads the iterative deepening search method to explore fewer levels.