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 
, 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 
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Apt, K.R., Wallace, M.: Constraint logic programming using ECLiPSe. Cambridge University Press (2007)
Hoder, K., Voronkov, A.: Comparing unification algorithms in first-order theorem proving. In: Mertsching, B., Hund, M., Aziz, Z. (eds.) KI 2009. LNCS, vol. 5803, pp. 435–443. Springer, Heidelberg (2009)
Kaliszyk, C., Schulz, S., Urban, J., Vyskočil, J.: System description: E.T. 0.1. In: Conference on Automated Deduction, LNCS. Springer (2015, to appear)
Kaliszyk, C., Urban, J., Vyskočil, J.: Certified connection tableaux proofs for HOL Light and TPTP. In: Leroy, X., Tiu, A. (eds.) Proc. of the 4th Conference on Certified Programs and Proofs (CPP 2015), pp. 59–66. ACM (2015)
Korovin, K.: iProver – an instantiation-based theorem prover for first-order logic (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 292–298. Springer, Heidelberg (2008)
Kovács, L., Voronkov, A.: First-order theorem proving and vampire. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 1–35. Springer, Heidelberg (2013)
Letz, R., Stenz, G.: Model elimination and connection tableau procedures. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vols. 2, pp. 2015–2114. Elsevier and MIT Press (2001)
Moser, M., Ibens, O., Letz, R., Steinbach, J., Goller, C., Schumann, J., Mayr, K.: SETHEO and E-SETHEO – the CADE-13 systems. J. Autom. Reasoning 18(2), 237–246 (1997)
Otten, J.: Restricting backtracking in connection calculi. AI Commun. 23(2-3), 159–182 (2010)
Otten, J., Bibel, W.: leanCoP: lean connection-based theorem proving. J. Symb. Comput. 36(1-2), 139–161 (2003)
Raths, T., Otten, J.: randocop: Randomizing the proof search order in the connection calculus. In: Konev, B., Schmidt, R.A., Schulz, S. (eds.) Proceedings of the First International Workshop on Practical Aspects of Automated Reasoning, Sydney, Australia, August 10-11. CEUR Workshop Proceedings, vol. 373, CEUR-WS.org. (2008)
Robinson, J.A.: A machine-oriented logic based on the resolution principle. J. ACM 12(1), 23–41 (1965)
Schulz, S.: System description: E 1.8. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR-19 2013. LNCS, vol. 8312, pp. 735–743. Springer, Heidelberg (2013)
Sutcliffe, G.: The 4th IJCAR automated theorem proving system competition - CASC-J4. AI Commun. 22(1), 59–72 (2009)
Sutcliffe, G.: The 6th IJCAR automated theorem proving system competition - CASC-J6. AI Commun. 26(2), 211–223 (2013)
Urban, J., Vyskočil, J., Štěpánek, P.: MaLeCoP machine learning connection prover. In: Brünnler, K., Metcalfe, G. (eds.) TABLEAUX 2011. LNCS, vol. 6793, pp. 263–277. Springer, Heidelberg (2011)
Wielemaker, J., Schrijvers, T., Triska, M., Lager, T.: SWI-Prolog. TPLP 12(1-2), 67–96 (2012)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Kaliszyk, C. (2015). Efficient Low-Level Connection Tableaux. In: De Nivelle, H. (eds) Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 2015. Lecture Notes in Computer Science(), vol 9323. Springer, Cham. https://doi.org/10.1007/978-3-319-24312-2_8
Download citation
DOI: https://doi.org/10.1007/978-3-319-24312-2_8
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-24311-5
Online ISBN: 978-3-319-24312-2
eBook Packages: Computer ScienceComputer Science (R0)