×

zbMATH — the first resource for mathematics

Semantically-guided goal-sensitive reasoning: inference system and completeness. (English) Zbl 1437.68189
Summary: We present a new method for clausal theorem proving, named SGGS from semantically-guided goal-sensitive reasoning. SGGS generalizes to first-order logic the conflict-driven clause learning (CDCL) procedure for propositional satisfiability. Starting from an initial interpretation, used for semantic guidance, SGGS employs a sequence of constrained clauses to represent a candidate model, instance generation to extend it, resolution and other inferences to explain and solve conflicts, amending the model. We prove that SGGS is refutationally complete and model complete in the limit, regardless of initial interpretation. SGGS is also goal sensitive, if the initial interpretation is properly chosen, and proof confluent, because it repairs the current model without undoing steps by backtracking. Thus, SGGS is a complete first-order method that is simultaneously model-based à la CDCL, semantically-guided, goal-sensitive, and proof confluent.

MSC:
68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
03B35 Mechanization of proofs and logical operations
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Alagi, G; Weidenbach, C; Lutz, C (ed.); Ranise, S (ed.), NRCL—a model building approach to the bernays-schönfinkel fragment, No. 9322, 69-84, (2015), Berlin · Zbl 06688808
[2] Baumgartner, P; Swart, H (ed.), Hyper tableaux—the next generation, No. 1397, 60-76, (1998), Berlin · Zbl 0910.03007
[3] Baumgartner, P; McAllester, D (ed.), FDPLL—a first-order Davis-Putnam-logeman-loveland procedure, No. 1831, 200-219, (2000), Berlin · Zbl 0963.68182
[4] Baumgartner, P; Pfenning, F (ed.), Logical engineering with instance-based methods, No. 4603, 404-409, (2007), Berlin
[5] Baumgartner, P; Fuchs, A; Tinelli, C, Implementing the model evolution calculus, Int. J. Artif. Intell. Tools, 15, 21-52, (2006) · Zbl 1165.03308
[6] Baumgartner, P; Fuchs, A; Tinelli, C; Hermann, M (ed.); Voronkov, A (ed.), Lemma learning in the model evolution calculus, No. 4246, 572-586, (2006), Berlin · Zbl 1165.03308
[7] Baumgartner, P; Pelzer, B; Tinelli, C, Model evolution calculus with equality—revised and implemented, J. Symb. Comput., 47, 1011-1045, (2012) · Zbl 1258.03020
[8] Baumgartner, P; Tinelli, C, The model evolution calculus as a first-order DPLL method, Artif. Intell., 172, 591-632, (2008) · Zbl 1182.03034
[9] Baumgartner, P; Waldmann, U; Schmidt, R (ed.), Superposition and model evolution combined, No. 5663, 17-34, (2009), Berlin · Zbl 1237.03010
[10] Bender, M; Pelzer, B; Schon, C; Bonacina, MP (ed.), E-krhyper 1.4: extensions for unique names and description logic, No. 7898, 126-134, (2013), Berlin · Zbl 1381.68258
[11] Billon, J-P; Miglioli, P (ed.); Moscato, U (ed.); Mundici, D (ed.); Ornaghi, M (ed.), The disconnection method, No. 1071, 110-126, (1996), Berlin
[12] Bonacina, MP; Wooldridge, MJ (ed.); Veloso, M (ed.), A taxonomy of theorem-proving strategies, No. 1600, 43-84, (1999), Berlin · Zbl 0984.03011
[13] Bonacina, MP; Echenim, M, Theory decision by decomposition, J. Symb. Comput., 45, 229-260, (2010) · Zbl 1192.68626
[14] Bonacina, MP; Furbach, U; Sofronie-Stokkermans, V; Martí-Oliet, N (ed.); Olveczky, P (ed.); Talcott, C (ed.), On first-order model-based reasoning, No. 9200, 181-204, (2015), Berlin · Zbl 1322.03013
[15] Bonacina, MP; Lynch, CA; Moura, L, On deciding satisfiability by theorem proving with speculative inferences, J. Autom. Reason., 47, 161-189, (2011) · Zbl 1243.68265
[16] Bonacina, M.P., Plaisted, D.A: Constraint manipulation in SGGS. In: Kutsia, T., Ringeissen, C. (eds.) Proceedings of the 28th Workshop on Unification (UNIF). Technical Reports of the Research Institute for Symbolic Computation, pp. 47-54. Johannes Kepler Universität, July (2014). http://vsl2014.at/meetings/UNIF-index.html · Zbl 1137.03306
[17] Bonacina, M.P., Plaisted, D.A.: SGGS theorem proving: an exposition. In: Schulz, S., De Moura, L., Konev, B. (eds.) Proceedings of the 4th Workshop on Practical Aspects in Automated Reasoning (PAAR) (2014). EasyChair Proceedings in Computing (EPiC), vol. 31, pp. 25-38 (2015) · Zbl 0959.68115
[18] Bonacina, MP; Plaisted, DA, Semantically-guided goal-sensitive reasoning: model representation, J. Autom. Reason., 56, 113-141, (2016) · Zbl 1356.68180
[19] Chang, C.-L., Lee, R.C.-T.: Symbolic Logic and Mechanical Theorem Proving. Academic Press, Cambridge (1973) · Zbl 0263.68046
[20] Chu, H; Plaisted, DA, Model finding in semantically guided instance-based theorem proving, Fundam. Inform., 21, 221-235, (1994) · Zbl 0938.68818
[21] Chu, H; Plaisted, DA, CLINS-S: a semantically guided first-order theorem prover, J. Autom. Reason., 18, 183-188, (1997)
[22] Comon, H; Lassez, J-L (ed.); Plotkin, G (ed.), Disunification: a survey, 322-359, (1991), Cambridge
[23] Comon, H; Lescanne, P, Equational problems and disunification, J. Symb. Comput., 7, 371-425, (1989) · Zbl 0678.68093
[24] Davis, M.: The Universal Computer. The Road from Leibniz to Turing. Turing Centenary Edition. Mathematics/Logic/Computing Series. CRC Press, Taylor and Francis Group (2012) · Zbl 1243.68013
[25] Davis, M; Logemann, G; Loveland, D, A machine program for theorem-proving, Commun. ACM, 5, 394-397, (1962) · Zbl 0217.54002
[26] Davis, M; Putnam, H, A computing procedure for quantification theory, J. ACM, 7, 201-215, (1960) · Zbl 0212.34203
[27] Moura, L; Bjørner, N; Armando, A (ed.); Baumgartner, P (ed.); Dowek, G (ed.), Engineering DPLL(T) + saturation, No. 5195, 475-490, (2008), Berlin · Zbl 1165.68479
[28] Fietzke, A.: Labelled superposition. PhD thesis, Max Planck Institut für Informatik, Saabrücken, October (2013) · Zbl 0135.18401
[29] Fietzke, A; Weidenbach, C; Armando, A (ed.); Baumgartner, P (ed.); Dowek, G (ed.), Labelled splitting, No. 5195, 459-474, (2008), Berlin · Zbl 1165.03314
[30] Ganzinger, H., Korovin, K.: New directions in instantiation-based theorem proving. In: Proceedings of the 18th IEEE Symposium on Logic in Computer Science (LICS), pp. 55-64. IEEE Computer Society Press (2003)
[31] Ganzinger, H; Korovin, K; Hermann, M (ed.); Voronkov, A (ed.), Theory instantiation, No. 4246, 497-511, (2006), Berlin · Zbl 1165.03315
[32] Hoder, K; Voronkov, A; Bonacina, MP (ed.), The 481 ways to split a clause and deal with propositional variables, No. 7898, 450-464, (2013), Berlin · Zbl 1382.68216
[33] Jacobs, S; Waldmann, U, Comparing instance generation methods for automated reasoning, J. Autom. Reason., 38, 57-78, (2007) · Zbl 1113.68089
[34] Knuth, DE; Bendix, PB; Leech, J (ed.), Simple word problems in universal algebras, 263-298, (1970), Oxford
[35] Korovin, K; Schmidt, R (ed.), An invitation to instantiation-based reasoning: from theory to practice, No. 5663, 163-166, (2009), Berlin
[36] Korovin, K; Voronkov, A (ed.); Weidenbach, C (ed.), Inst-gen: a modular approach to instantiation-based automated reasoning, No. 7797, 239-270, (2013), Berlin · Zbl 1385.68038
[37] Korovin, K; Sticksel, C; Giesl, J (ed.); Hähnle, R (ed.), Iprover-eq: an instantiation-based theorem prover with equality, No. 6173, 196-202, (2010), Berlin · Zbl 1291.68354
[38] Kovàcs, L; Voronkov, A; Sharygina, N (ed.); Veith, H (ed.), First order theorem proving and vampire, No. 8044, 1-35, (2013), Berlin
[39] Lee, S-J; Plaisted, DA, Eliminating duplication with the hyperlinking strategy, J. Autom. Reason., 9, 25-42, (1992) · Zbl 0784.68077
[40] Letz, R; Stenz, G; Goré, RP (ed.); Leitsch, A (ed.); Nipkow, T (ed.), DCTP—a disconnection calculus theorem prover, No. 2083, 381-385, (2001), Berlin · Zbl 0988.68589
[41] Letz, R; Stenz, G; Nieuwenhuis, R (ed.); Voronkov, A (ed.), Proof and model generation with disconnection tableaux, No. 2250, 142-156, (2001), Berlin · Zbl 1275.03081
[42] Letz, R; Stenz, G; Egly, U (ed.); Fermüller, CG (ed.), Integration of equality reasoning into the disconnection calculus, No. 2381, 176-190, (2002), Berlin · Zbl 1015.68172
[43] Ludwig, M; Waldmann, U; Dershowitz, N (ed.); Voronkov, A (ed.), An extension of the Knuth-bendix ordering with LPO-like properties, No. 4790, 348-362, (2007), Berlin · Zbl 1137.03306
[44] Maher, M.J.: Complete axiomatizations of the algebras of finite, rational and infinite trees. Technical report, IBM Thomas J. Watson Research Center, Yorktown Heights, NY, USA (1988) · Zbl 1182.03034
[45] Maher, M.J.: Complete axiomatizations of the algebras of finite, rational and infinite trees. In: Proceedings of the 3rd Annual IEEE Symposium on Logic in Computer Science (LICS), pp. 348-457. IEEE Computer Society Press (1988)
[46] Malik, S; Zhang, L, Boolean satisfiability: from theoretical hardness to practical success, Commun. ACM, 52, 76-82, (2009)
[47] Manthey, R; Bry, F; Lusk, E (ed.); Overbeek, R (ed.), SATCHMO: a theorem prover implemented in prolog, No. 310, 415-434, (1988), Berlin · Zbl 0668.68104
[48] Marques Silva, J.P., Lynce, I., Malik, S.: Conflict-driven clause learning SAT solvers. In: Biere, A., Heule, M., Van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, vol. 185, pp. 131-153. IOS Press (2009)
[49] Marques Silva, JP; Sakallah, KA, GRASP: a search algorithm for propositional satisfiability, IEEE Trans. Comput., 48, 506-521, (1999) · Zbl 1392.68388
[50] McCune, W.W.: OTTER 3.0 reference manual and guide. Technical report 94/6, MCS Division, Argonne National Laboratory (1994)
[51] Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: Proceedings of the 39th Design Automation Conference (DAC), pp. 530-535 (2001) · Zbl 1243.68265
[52] Piskac, R; Moura, L; Bjørner, N, Deciding effectively propositional logic using DPLL and substitution sets, J. Autom. Reason., 44, 401-424, (2010) · Zbl 1197.03011
[53] Plaisted, DA; Banerji, RB (ed.), Mechanical theorem proving, 269-320, (1990), Amsterdam
[54] Plaisted, DA; Miller, S; Voronkov, A (ed.); Weidenbach, C (ed.), The relative power of semantics and unification, No. 7797, 317-344, (2013), Berlin · Zbl 1383.68081
[55] Plaisted, DA; Zhu, Y, Ordered semantic hyper linking, J. Autom. Reason., 25, 167-217, (2000) · Zbl 0959.68115
[56] Reger, G; Suda, M; Voronkov, A; Felty, AP (ed.); Middeldorp, A (ed.), Playing with AVATAR, No. 9195, 399-415, (2015), Berlin · Zbl 06515522
[57] Riazanov, A.: Implementing an efficient theorem prover. PhD thesis, Department of Computer Science, The University of Manchester (July 2003) · Zbl 0910.03007
[58] Robinson, AJ, Automatic deduction with hyper-resolution, Int. J. Comput. Math., 1, 227-234, (1965) · Zbl 0158.26003
[59] Schulz, S; McMillan, K (ed.); Middeldorp, A (ed.); Voronkov, A (ed.), System description: E 1.8, No. 8312, 735-743, (2013), Berlin · Zbl 1407.68442
[60] Slagle, JR, Automatic theorem proving with renamable and semantic resolution, J. ACM, 14, 687-697, (1967) · Zbl 0157.02405
[61] Weidenbach, C; Robinson, A (ed.); Voronkov, A (ed.), Combining superposition, sorts and splitting, No. 2, 1965-2012, (2001), Amsterdam · Zbl 1011.68129
[62] Weidenbach, C; Dimova, D; Fietzke, A; Kumar, R; Suda, M; Wischnewski, P; Schmidt, R (ed.), SPASS version 3.5, No. 5663, 140-145, (2009), Berlin
[63] Wos, L; Carson, D; Robinson, G, Efficiency and completeness of the set of support strategy in theorem proving, J. ACM, 12, 536-541, (1965) · Zbl 0135.18401
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.