×

Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning. (English) Zbl 1425.68379

Summary: This paper defines the (first-order) conflict resolution calculus: an extension of the resolution calculus inspired by techniques used in modern Sat-solvers. The resolution inference rule is restricted to (first-order) unit propagation and the calculus is extended with a mechanism for assuming decision literals and with a new inference rule for clause learning, which is a first-order generalization of the propositional conflict-driven clause learning procedure. The calculus is sound (because it can be simulated by natural deduction) and refutationally complete (because it can simulate resolution), and these facts are proven in detail here.

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
03B35 Mechanization of proofs and logical operations
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
PDFBibTeX XMLCite
Full Text: DOI arXiv

References:

[1] Alagi, G., Weidenbach, C.: Non-redundant clause learning. In: FroCoS, pp. 69-84 (2015) · Zbl 0336.68037
[2] Beth, E.W.: Semantic entailment and formal derivability. In: Mededelingen van de Koninklijke Nederlandse Akademie van Wetenschappen, Afdeling Letterkunde 18(13), 309-342 (1955)
[3] Bachmair, L., Ganzinger, H.: Completion of first-order clauses with equality by strict superposition (Extended Abstract). In: 2nd International Workshop Conditional and Typed Rewriting Systems, LNCS 516, pp. 162-180. Springer, Berlin (1990) · Zbl 1507.03068
[4] Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification. J. Log. Comput. 4(3), 217-247 (1994) · Zbl 0814.68117 · doi:10.1093/logcom/4.3.217
[5] Baumgartner, P.: A first order Davis-Putnam-Longeman-Loveland procedure. In: Proceedings of the 17th International Conference on Automated Deduction (CADE), pp. 200-219 (2000) · Zbl 0963.68182
[6] Baumgartner, P.: Model evolution based theorem proving. IEEE Intel. Syst. 29(1), 4-10 (2014) · doi:10.1109/MIS.2013.124
[7] Baumgartner, P., Tinelli, C.: The model evolution calculus. In: CADE, pp. 350-364 (2003) · Zbl 1278.68249
[8] Baumgartner, P., Fuchs, A., Tinelli, C.: Lemma learning in the model evolution calculus. In: LPAR, pp. 572-586 (2006) · Zbl 1165.03308
[9] Biere, A.: PicoSAT Essentials. JSAT 4(2-4), 75-97 (2008) · Zbl 1159.68403
[10] Bonacina, M.P.: Plaisted, DA.: SGGS theorem proving: an exposition. In: Schulz, S., de Moura, L., Konev, B. (eds.) 4th Workshop on Practical Aspects of Automated Reasoning, PAAR@IJCAR 2014, Vienna, Austria, 2014, vol. 31, pp. 25-38. EasyChair (2014)
[11] Bonacina, M.P., Plaisted, D.A.: Semantically-guided goal-sensitive reasoning: model representation. J. Autom. Reason. 56(2), 113-141 (2016) · Zbl 1356.68180
[12] Brown, CE.: Satallax: An automatic higher-order prover. In: IJCAR, pp. 111-117 (2012) · Zbl 1358.68250
[13] Brown, CE.: Reducing higher-order theorem proving to a sequence of SAT problems. J. Autom. Reason. 51(1), 57-77 (2013) · Zbl 1314.68276
[14] Claessen, K.: The anatomy of equinox—an extensible automated reasoning tool for first-order logic and beyond (Talk Abstract). In: Proceedings of the 23rd International Conference on Automated Deduction (CADE-23), pp. 1-3 (2011) · Zbl 1341.68186
[15] Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM 7, 201-215 (1960) · Zbl 0212.34203 · doi:10.1145/321033.321034
[16] Davis, M., Logemann, G., Loveland, D.: A machine program for theorem proving. Commun. ACM 5(7), 394-397 (1962) · Zbl 0217.54002 · doi:10.1145/368273.368557
[17] de Nivelle, H., Meng, J.: Geometric resolution: a proof procedure based on finite model search. In: 3rd International Joint Conference on Automated Reasoning (IJCAR), pp. 303-317 (2006) · Zbl 1222.68378
[18] Gentzen, G.: Untersuchungen über das logische Schließen I & II. Math. Z. 39(1), 176-210, 405-431 (1935) · Zbl 0010.14501
[19] Barbosa, H., Fontaine, P.: Congruence closure with free variables (Work in Progress). In: 2nd International Workshop on Quantification (2015) · Zbl 1021.68082
[20] Korovin, K.: iProver—an instantiation-based theorem prover for first-order logic (system description)”. In: International Joint Conference on Automated Reasoning (IJCAR), pp. 292-298 (2008) · Zbl 1165.68462
[21] Korovin, K.: Inst-gen—a modular approach to instantiation-based automated reasoning. In: Voronkov, A., Weidenbach, C. (eds.) Programming Logics, vol. 7797, pp. 239-270. Springer, Berlin (2013) · Zbl 1385.68038
[22] Marques-Silva, J., Sakallah, K.A.: GRASP—a new search algorithm for satisfiability. In: International Conference on Computer-Aided Design, pp. 220-227 (1996)
[23] Marques-Silva, J., Lynce, I., Malik, S.: Conflict-driven clause learning SAT solvers. In: Handbook of Satisfiability, pp. 127-149 (2008) · Zbl 0212.34203
[24] McCharen, J., Overbeek, R., Wos, L.: Complexity and related enhancements for automated theorem-proving programs. Comput. Math. Appl. 2, 1-16 (1976) · Zbl 0336.68037
[25] McCune, W.: Prover9 Manual (2009). https://www.cs.unm.edu/ mccune/prover9/manual/2009-11A/ · Zbl 0217.54002
[26] Riazanov, A., Voronkov, A.: The design and implementation of VAMPIRE. AI Commun. 15(2-3), 91-110 (2002) · Zbl 1021.68082
[27] Robinson, J.A.: A machine-oriented logic based on the resolution principle. J. ACM 12(1), 23-41 (1965) · Zbl 0139.12303 · doi:10.1145/321250.321253
[28] Robinson, G., Wos, L.: Paramodulation and theorem-proving in first-order thories with equality. Mach. Intell. 4, 135-150 (1969) · Zbl 0219.68047
[29] Schultz, S.: System description: E 1.8. In: LPAR, pp. 735-743 (2013) · Zbl 1407.68442
[30] Sutcliffe, G.: The TPTP problem library and associated infrastructure: the FOF and CNF parts, v3.5.0. J. Autom. Reason. 43(4), 337-362 (2009) · Zbl 1185.68636 · doi:10.1007/s10817-009-9143-8
[31] Voronkov, A.: AVATAR: The architecture for first-order theorem provers. In: CAV, pp. 696-710 (2014) · Zbl 1495.68240
[32] Waldmann, U.: Superposition. In: Paleo, B.W. (eds.) Towards an Encyclopaedia of Proof Systems, p. 29. College Publications, London, UK (2017)
[33] Waldmann, U.: Saturation with redundancy. In: Paleo, B.W. (eds.) Towards an Encyclopaedia of Proof Systems, p. 30. College Publications, London, UK (2017)
[34] Weidenbach, C.: Combining superposition, sorts and splitting. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 1965-2013. Elsevier and MIT Press (2001) · Zbl 1011.68129
[35] Weidenbach, C.: The Theory of SPASS version 2.0. In: SPASS 2.0 documentation · Zbl 1072.68596
[36] Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: SPASS Version 3.5. In: CADE, pp. 140-145 (2009)
[37] Wetzler, N., Heule, M., Hunt Jr, WA.: DRAT-trim: Efficient checking and trimming using expressive clausal proofs. In: SAT, pp. 422-429 (2014) · Zbl 1423.68475
[38] Zhang, L., Madigan, CF., Moskewicz, MH., Malik, S.: Efficient conflict driven learning in a Boolean satisfiability solver. In: International Conference on Computer-Aided Design, pp. 279-285 (2001)
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.