Abstract

Many tableaux provers that follow Stickel’s Prolog Technology and lean have been relying on the Prolog compiler for an efficient term representation and the implementation of unification. In particular, this is the case for leanCOP, the only tableaux prover that regularly takes part in the CASC, the yearly ATP competition. On the other hand, the most efficient superposition provers are typically written in low-level languages, reckoning that the efficiency factor is significant.

In this paper we discuss low-level representations for first-order tableaux theorem proving and present the Bare Metal Tableaux Prover, a C implementation of the exact calculus used in the leanCoP theorem prover with its cut semantics. The data structures are designed in such a way that the prove function does not need to allocate any memory. The code is less elegant than the Prolog code, albeit concise and readable. We also measure the constant factor that a high-level programming language incurs: the low-level implementation performs 18 times more inferences per second on an average TPTP CNF problem. We also discuss the implementation improvements which could be enabled by complete access to the internal data structures, such as direct manipulation of backtracking points.

BibTeX

@inproceedings{CK-TABLEAUX15,
  author    = "Cezary Kaliszyk",
  title     = "Efficient Low-Level Connection Tableaux",
  booktitle = "Proceedings of the 24th International Conference on
               Automated Reasoning with Analytic Tableaux and Related
               Methods (TABLEAUX 2015)",
  editor    = "Hans de Nivelle",
  series    = "Lecture Notes in Artificial Intelligence",
  volume    = 9323,
  pages     = "102--111",
  year      = 2015,
  doi       = "10.1007/978-3-319-24312-2_8"
}