Download PDFOpen PDF in browser

Implementing Bottom-up Procedures with Code Trees: a Case Study of Forward Subsumption

EasyChair Preprint no. 3148

35 pagesDate: April 12, 2020

Abstract

This preprint is a reprint of an Uppsala University Technical Report published on October 3, 1994. Below we give the original abstract. As it turned out, it was the first ever implementation of runtime algorithm specialization.

Orignal Abstract. 

We present an implementation technique for a class of bottom-up logic procedures. The technique is based on code trees. It is intended to speed up most important and costly operations, such as subsumption and resolution. As a case study, we consider the forward subsumption problem which is the bottleneck of many systems implementing first order logic.

In order to efficiently implement subsumption, we specialize subsumption algorithms at run time, using the abstract subsumption machine. The abstract subsumption machine makes subsumption-check using sequences of instructions that are similar to the Warren Abstract Machine instructions. It gives an efficient implementation of the ``clause at a time'' subsumption problem. To implement subsumption on the ``set at a time'' basis we combine sequences of instructions in code trees.

We show that this technique yields a new way of indexing clauses. Some experimental results are given.

The code trees technique may be used in various procedures, including binary resolution, hyperresolution, UR-resolution, the inverse method, paramodulation and rewriting, OLDT-resolution, SLD-AL-resolution, bottom-up evaluation of logic programs and disjunctive logic programs.

Keyphrases: code trees, first-order theorem proving, forward subsumption, runtime algorithm specialization, Saturation Algorithms, Subsumption algorithm, term indexing

BibTeX entry
BibTeX does not have the right entry for preprints. This is a hack for producing the correct reference:
@Booklet{EasyChair:3148,
  author = {Andrei Voronkov},
  title = {Implementing Bottom-up Procedures with Code Trees: a Case Study of Forward Subsumption},
  howpublished = {EasyChair Preprint no. 3148},

  year = {EasyChair, 2020}}
Download PDFOpen PDF in browser