Optimizing Proof Search in Model Elimination

John Harrison.

Proceedings of the 13th International Conference on Automated Deduction (CADE'13), Springer LNCS 1104, pp. 313-327, 1996. Longer version is also available as TUCS Technical Report number 6.

Abstract:

Many implementations of model elimination perform proof search by iteratively increasing a bound on the total size of the proof. We propose an optimized version of this search mode using a simple divide-and-conquer refinement. Optimized and unoptimized modes are compared, together with depth-bounded and best-first search, over the entire TPTP problem library. The optimized size-bounded mode seems to be the overall winner, but for each strategy there are problems on which it performs best. Some attempt is made to analyze why. We emphasize that our optimization, and other implementation techniques like caching, are rather general: they are not dependent on the details of model elimination, or even that the search is concerned with theorem proving. As such, we believe that this study is a useful complement to research on extending the model elimination calculus.

DVI or PostScript or PDF

DVI (Times font) or PostScript (Times font)

Full list of results (text)

Bibtex entry:

@INPROCEEDINGS{harrison-me,
        author          = "John Harrison",
        title           = "Optimizing Proof Search in Model Elimination",
        booktitle       = "13th International Conference on
                           Automated Deduction",
        editor          = "M. A. McRobbie and J. K. Slaney",
        address         = "New Brunswick, NJ",
        date            = "30 July -- 3 August 1996",
        year            = 1996,
        series          = "Lecture Notes in Computer Science",
        volume          = 1104,
        pages           = "313--327",
        publisher       = "Springer-Verlag"}