Abstract
We define a superposition calculus with explicit splitting on the basis of labelled clauses. For the first time we show a superposition calculus with an explicit non-chronological backtracking rule sound and complete. The new backtracking rule advances backtracking with branch condensing known from SPASS. An experimental evaluation of an implementation of the new rule shows that it improves considerably on the previous SPASS splitting implementation. Finally, we discuss the relationship between labelled first-order splitting and DPLL style splitting with intelligent backtracking and clause learning.
Article PDF
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.Avoid common mistakes on your manuscript.
References
Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)
Bachmair, L., Ganzinger, H.: Resolution theorem proving. In: Handbook of Automated Reasoning, pp. 19–99 (2001)
Bachmair, L., Ganzinger, H., Waldmann, U.: Superposition with simplification as a decision procedure for the monadic class with equality. In: Gottlob, G., Leitsch, A., Mundici, D. (eds.) Computational Logic and Proof Theory, Third Kurt Gödel Colloquium. LNCS, vol. 713, pp. 83–96. Springer, New York (1993)
Basin, D., D’Agostino, M., Gabbay, D.M., Matthews, S., Viganó, L., (eds.) Labelled Deduction. Kluwer, Dordrecht (2000)
Baumgartner, P., Tinelli, C.: The model evolution calculus as a first-order DPLL method. Artif. Intell. 172(4–5), 591–632 (2008)
Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM 7(3), 201–215 (1960)
de Nivelle, H.: Splitting through new proposition symbols. In: Logic for Programming, Artificial Intelligence, and Reasoning, 8th International Conference, LPAR 2001. LNAI, vol. 2250, pp. 172–185. Springer, New York (2001)
Eén, N., Sörensson, N.: An extensible SAT solver. Theory and Applications of Satisfiability Testing, pp. 502–518 (2004)
Fermüller, C.G., Leitsch, A., Hustadt, U., Tamet, T.: Resolution decision procedures. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. II, chapter 25, pp. 1791–1849. Elsevier, Amsterdam (2001)
Fietzke, A., Weidenbach, C.: Labelled splitting. In: 4th International Joint Conference on Automated Reasoning (IJCAR). LNAI, vol. 5195, pp. 459–474. Springer, New York (2008)
Hillenbrand, T., Weidenbach, C.: Superposition for finite domains. Research report MPI-I-2007-RG1-002, Max-Planck Institute for Informatics, Saarbrücken (2007)
Lev-Ami, T., Weidenbach, C., Reps, T., Sagiv, M.: Labelled clauses. In: 21st International Conference on Automated Deduction (CADE-21). Lecture Notes in Computer Science, vol. 4603, pp. 311–327. Springer, New York (2007)
Nieuwenhuis, R., Oliveras, A.: Decision procedures for SAT, SAT Modulo Theories and Beyond. The Barcelogic Tools. (Invited Paper). In: Sutcliffe, G., Voronkov, A. (eds.) 12th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, LPAR’05. Lecture Notes in Computer Science, vol. 3835, pp. 23–46. Springer, New York (2005)
Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: from an abstract Davis–Putnam–Logemann–Loveland procedure to DPLL. J. ACM 53(6), 937–977 (2006)
Nieuwenhuis, R., Rubio, A.: Paramodulation-based theorem proving. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. I, chapter 7, pp. 371–443. Elsevier, Amsterdam (2001)
Nonnengart, A. Weidenbach, C.: Computing small clause normal forms. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. 1, chapter 6, pp. 335–367. Elsevier, Amsterdam (2001)
Riazanov, A., Voronkov, A.: Splitting without backtracking. In: IJCAI, pp. 611–617 (2001)
Sutcliffe, G., Suttner, C.: The TPTP problem library: CNF release v1.2.1. J Autom Reason 21(2), 177–203 (1998)
Tseitin, G.: On the complexity of derivations in propositional calculus. In: Siekmann, J., Wrightson, G. (eds.) Automation of Reasoning: Classical Papers on Computational Logic, vol. 2, pp. 466–483. Springer (1983). First published in: Studies in Constructive Mathematics and Mathematical Logic, (Slisenko, A.O., ed.) (1968)
Weidenbach, C.: Combining superposition, sorts and splitting. In: Robinson, A., Voronkov, A. (eds.), Handbook of Automated Reasoning, vol. 2, chapter 27, pp. 1965–2012. Elsevier, Amsterdam (2001)
Weidenbach, C., Gaede, B., Rock, G.: Spass and flotter, version 0.42. In: McRobbie, M., Slaney, J. (eds.) 13th International Conference on Automated Deduction, CADE-13. LNAI, vol. 1104, pp. 141–145. Springer, New York (1996)
Weidenbach, C., Schmidt, R., Hillenbrand, T., Rusev, R., Topic, D.: System description: SPASS version 3.0. In: Pfenning, F. (ed.) CADE-21: 21st International Conference on Automated Deduction. LNAI, vol. 4603, pp. 514–520. Springer, New York (2007)
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
Open Access This is an open access article distributed under the terms of the Creative Commons Attribution Noncommercial License ( https://creativecommons.org/licenses/by-nc/2.0 ), which permits any noncommercial use, distribution, and reproduction in any medium, provided the original author(s) and source are credited.
About this article
Cite this article
Fietzke, A., Weidenbach, C. Labelled splitting. Ann Math Artif Intell 55, 3–34 (2009). https://doi.org/10.1007/s10472-009-9150-9
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10472-009-9150-9