Formalizing Bachmair and Ganzinger’s ordered resolution prover. (English) Zbl 1468.68307

Summary: We present an Isabelle/HOL formalization of the first half of Bachmair and Ganzinger’s chapter on resolution theorem proving, culminating with a refutationally complete first-order prover based on ordered resolution with literal selection. We developed general infrastructure and methodology that can form the basis of completeness proofs for related calculi, including superposition. Our work clarifies fine points in the chapter, emphasizing the value of formal proofs in the field of automated reasoning.


68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
03B35 Mechanization of proofs and logical operations
68V20 Formalization of mathematics in connection with theorem provers
Full Text: DOI Link


[1] Bachmair, L.; Dershowitz, N.; Plaisted, DA; Aït-Kaci, H.; Nivat, M., Completion without failure, Rewriting Techniques—Resolution of Equations in Algebraic Structures, 1-30 (1989), London: Academic Press, London
[2] Bachmair, L.; Ganzinger, H., Rewrite-based equational theorem proving with selection and simplification, J. Log. Comput., 4, 3, 217-247 (1994) · Zbl 0814.68117
[3] Bachmair, L.; Ganzinger, H., Ordered chaining calculi for first-order theories of transitive relations, J. ACM, 45, 6, 1007-1049 (1998) · Zbl 1065.68615
[4] Bachmair, L.; Ganzinger, H.; Robinson, A.; Voronkov, A., Resolution theorem proving, Handbook of Automated Reasoning, 19-99 (2001), Amsterdam: Elsevier, Amsterdam · Zbl 0993.03008
[5] Ballarin, C., Locales: a module system for mathematical theories, J. Autom. Reason., 52, 2, 123-153 (2014) · Zbl 1315.68218
[6] Baumgartner, P.; Waldmann, U.; Lutz, C.; Sattler, U.; Tinelli, C.; Turhan, A.; Wolter, F., Hierarchic superposition revisited, Description Logic, Theory Combination, and All That—Essays Dedicated to Franz Baader on the Occasion of His 60th Birthday, 15-56 (2019), Berlin: Springer, Berlin · Zbl 1443.68212
[7] Bentkamp, A.; Blanchette, J.; Tourret, S.; Vukmirović, P.; Waldmann, U.; Fontaine, P., Superposition with lambdas, CADE-27, LNCS, 55-73 (2019), Berlin: Springer, Berlin · Zbl 1471.03014
[8] Biendarra, J.; Blanchette, JC; Bouzy, A.; Desharnais, M.; Fleury, M.; Hölzl, J.; Kuncar, O.; Lochbihler, A.; Meier, F.; Panny, L.; Popescu, A.; Sternagel, C.; Thiemann, R.; Traytel, D.; Dixon, C.; Finger, M., Foundational (co)datatypes and (co)recursion for higher-order logic, FroCoS 2017, LNCS, 3-21 (2017), Berlin: Springer, Berlin · Zbl 06821624
[9] Blanchette, J.C.: Formalizing the metatheory of logical calculi and automatic provers in Isabelle/HOL (invited talk). In: Mahboubi, A., Myreen, M.O. (eds.) CPP 2019, pp. 1-13. ACM (2019)
[10] Blanchette, JC; Fleury, M.; Lammich, P.; Weidenbach, C., A verified SAT solver framework with learn, forget, restart, and incrementality, J. Autom. Reason., 61, 3, 333-366 (2018) · Zbl 1448.68457
[11] Blanchette, J.C., Fleury, M., Traytel, D.: Nested multisets, hereditary multisets, and syntactic ordinals in Isabelle/HOL. In: Miller, D. (ed.) FSCD 2017, LIPIcs, vol. 84, pp. 11:1-11:18. Schloss Dagstuhl—Leibniz-Zentrum für Informatik (2017) · Zbl 1434.03025
[12] Blanchette, JC; Kaliszyk, C.; Paulson, LC; Urban, J., Hammering towards QED, J. Formaliz. Reason., 9, 1, 101-148 (2016) · Zbl 1451.68318
[13] Blanchette, JC; Popescu, A.; Traytel, D., Soundness and completeness proofs by coinductive methods, J. Autom. Reason., 58, 1, 149-179 (2017) · Zbl 1409.68251
[14] Brand, D., Proving theorems with the modification method, SIAM J. Comput., 4, 4, 412-430 (1975) · Zbl 0333.68059
[15] Cruanes, S.: Logtk: A logic toolkit for automated reasoning and its implementation. In: Schulz, S., de Moura, L., Konev, B. (eds.) PAAR-2014, EPiC Series in Computing, vol. 31, pp. 39-49. EasyChair (2014)
[16] Denzinger, J.; Kronenburg, M.; Schulz, S., DISCOUNT—a distributed and learning equational prover, J. Autom. Reason., 18, 2, 189-198 (1997)
[17] Dershowitz, N.; Manna, Z., Proving termination with multiset orderings, Commun. ACM, 22, 8, 465-476 (1979) · Zbl 0431.68016
[18] Fleury, M., Blanchette, J.C., Lammich, P.: A verified SAT solver with watched literals using Imperative HOL. In: Andronick, J., Felty, A.P. (eds.) CPP 2018, pp. 158-171. ACM (2018)
[19] Godoy, G.; Nieuwenhuis, R., Superposition with completely built-in abelian groups, J. Symb. Comput., 37, 1, 1-33 (2004) · Zbl 1043.03011
[20] Gordon, MJC; Melham, TF, Introduction to HOL: A Theorem Proving Environment for Higher Order Logic (1993), Cambridge: Cambridge University Press, Cambridge
[21] Hirokawa, N., Middeldorp, A., Sternagel, C., Winkler, S.: Infinite runs in abstract completion. In: Miller, D. (ed.) FSCD 2017, LIPIcs, vol. 84, pp. 19:1-19:16. Schloss Dagstuhl—Leibniz-Zentrum für Informatik (2017) · Zbl 1441.68113
[22] Krauss, A.; Furbach, U.; Shankar, N., Partial recursive functions in higher-order logic, IJCAR 2006, LNCS, 589-603 (2006), Berlin: Springer, Berlin · Zbl 1222.68367
[23] McCune, W.: Otter 2.0. In: Stickel, M.E. (ed.) CADE-10, LNCS, vol. 449, pp. 663-664. Springer, Berlin (1990)
[24] Nieuwenhuis, R.; Rubio, A., Theorem proving with ordering and equality constrained clauses, J. Symb. Comput., 19, 4, 321-351 (1995) · Zbl 0844.68107
[25] Nieuwenhuis, R.; Rubio, A.; Robinson, A.; Voronkov, A., Paramodulation-based theorem proving, Handbook of Automated Reasoning, 371-443 (2001), Amsterdam: Elsevier, Amsterdam · Zbl 0997.03012
[26] Nipkow, T.; Kuncak, V.; Rybalchenko, A., Teaching semantics with a proof assistant: no more LSD trip proofs, VMCAI 2012, LNCS, 24-38 (2012), Berlin: Springer, Berlin · Zbl 1325.68005
[27] Nipkow, T.; Klein, G., Concrete Semantics: With Isabelle/HOL (2014), Berlin: Springer, Berlin · Zbl 1410.68004
[28] Nipkow, T.; Paulson, LC; Wenzel, M., Isabelle/HOL: A Proof Assistant for Higher-Order Logic, LNCS (2002), Berlin: Springer, Berlin · Zbl 0994.68131
[29] O’Connor, R.; Hurd, J.; Melham, TF, Essential incompleteness of arithmetic verified by Coq, TPHOLs 2005, LNCS, 245-260 (2005), Berlin: Springer, Berlin · Zbl 1152.03315
[30] Paulson, LC, A machine-assisted proof of Gödel’s incompleteness theorems for the theory of hereditarily finite sets, Rew. Symb. Logic, 7, 3, 484-498 (2014) · Zbl 1337.03021
[31] Peltier, N.: A variant of the superposition calculus. Archive of Formal Proofs 2016 (2016). https://www.isa-afp.org/entries/SuperCalc.shtml. Accessed 22 May 2020
[32] Persson, H.: Constructive completeness of intuitionistic predicate logic—a formalisation in type theory. Licentiate thesis, Chalmers tekniska högskola and Göteborgs universitet (1996)
[33] Pierce, B.C.: Lambda, the ultimate TA: Using a proof assistant to teach programming language foundations. In: Hutton, G., Tolmach, A.P. (eds.) ICFP 2009, pp. 121-122. ACM (2009)
[34] Popescu, A.; Traytel, D.; Fontaine, P., A formally verified abstract account of Gödel’s incompleteness theorems, CADE-27, LNCS, 442-461 (2019), Berlin: Springer, Berlin · Zbl 07178991
[35] Reger, G., Suda, M.: Checkable proofs for first-order theorem proving. In: Reger, G., Traytel, D. (eds.) ARCADE 2017, EPiC Series in Computing, vol. 51, pp. 55-63. EasyChair (2017)
[36] Schlichtkrull, A., Formalization of the resolution calculus for first-order logic, J. Autom. Reason., 61, 4, 455-484 (2018) · Zbl 1451.03019
[37] Schlichtkrull, A., Blanchette, J.C., Traytel, D.: A verified prover based on ordered resolution. In: Mahboubi, A., Myreen, M.O. (eds.) CPP 2019, pp. 152-165. ACM (2019)
[38] Schlichtkrull, A., Blanchette, J.C., Traytel, D., Waldmann, U.: Formalization of a comprehensive framework for saturation theorem proving in Isabelle/HOL. Archive of Formal Proofs 2018 (2018). https://www.isa-afp.org/entries/Ordered_Resolution_Prover.html. Accessed 22 May 2020
[39] Schlichtkrull, A.; Blanchette, JC; Traytel, D.; Waldmann, U.; Galmiche, D.; Schulz, S.; Sebastiani, R., Formalizing Bachmair and Ganzinger’s ordered resolution prover, IJCAR 2018, LNCS, 89-107 (2018), Berlin: Springer, Berlin · Zbl 1468.68306
[40] Shankar, N., Towards mechanical metamathematics, J. Autom. Reason., 1, 4, 407-434 (1985) · Zbl 0616.68075
[41] Shankar, N., Metamathematics, Machines, and Gödel’s Proof, Cambridge Tracts in Theoretical Computer Science (1994), Cambridge: Cambridge University Press, Cambridge
[42] Sutcliffe, G.; Zimmer, J.; Schulz, S.; Zhang, W.; Sorge, V., TSTP data-exchange formats for automated theorem proving tools, Distributed Constraint Problem Solving and Reasoning in Multi-Agent Systems, Frontiers in Artificial Intelligence and Applications, 201-215 (2004), Amsterdam: IOS Press, Amsterdam
[43] Thiemann, R.; Sternagel, C.; Berghofer, S.; Nipkow, T.; Urban, C.; Wenzel, M., Certification of termination proofs using CeTA, TPHOLs 2009, LNCS, 452-468 (2009), Berlin: Springer, Berlin · Zbl 1252.68265
[44] Tourret, S.: A comprehensive framework for saturation theorem proving. Archive of Formal Proofs 2020 (2020). https://www.isa-afp.org/entries/Saturation_Framework.shtml. Accessed 22 May 2020
[45] Voronkov, A.; Biere, A.; Bloem, R., AVATAR: the architecture for first-order theorem provers, CAV 2014, LNCS, 696-710 (2014), Berlin: Springer, Berlin
[46] Waldmann, U.: Cancellative abelian monoids and related structures in refutational theorem proving (part I/II). J. Symb. Comput. 33(6), 777-829/831-861 (2002) · Zbl 1010.68166
[47] Waldmann, U.; Tourret, S.; Robillard, S.; Blanchette, J.; Peltier, N.; Sofronie-Stokkermans, V., A comprehensive framework for saturation theorem proving, IJCAR 2020 (2020), Berlin: LNCS. Springer, Berlin
[48] Wand, D.: Polymorphic + typeclass superposition. In: Schulz, S., de Moura, L., Konev, B. (eds.) PAAR-2014, EPiC Series in Computing, vol. 31, pp. 105-119. EasyChair (2014)
[49] Weidenbach, C.; Robinson, A.; Voronkov, A., Combining superposition, sorts and splitting, Handbook of Automated Reasoning, 1965-2013 (2001), Amsterdam: Elsevier, Amsterdam · Zbl 1011.68129
[50] Wenzel, M.: Isabelle/Isar—a generic framework for human-readable proof documents. In: Matuszewski, R. , Zalewska, A. (eds.) From Insight to Proof: Festschrift in Honour of Andrzej Trybulec, Studies in Logic, Grammar, and Rhetoric, vol. 10(23). University of Białystok (2007)
[51] Wenzel, M.; Jeuring, J.; Campbell, JA; Carette, J.; Reis, GD; Sojka, P.; Wenzel, M.; Sorge, V., Isabelle/jEdit-a prover IDE within the PIDE framework, CICM 2012, LNCS, 468-471 (2012), Berlin: Springer, Berlin · Zbl 1360.68769
[52] Zhang, H.; Kapur, D.; Lusk, EL; Overbeek, RA, First-order theorem proving using conditional rewrite rules, CADE-9, LNCS, 1-20 (1988), Berlin: Springer, Berlin
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.