×

A superposition calculus for abductive reasoning. (English) Zbl 1433.03023

Summary: We present a modification of the Superposition Calculus that is meant to generate consequences of sets of first-order axioms. This approach is proven to be sound and deductive-complete in the presence of redundancy elimination rules, provided the considered consequences are built on a given finite set of ground terms, represented by constant symbols. In contrast to other approaches, most existing results about the termination of the Superposition calculus can be carried over to our procedure. This ensures in particular that the calculus is terminating for many theories of interest to the SMT community.

MSC:

03B35 Mechanization of proofs and logical operations
68Q60 Specification and verification (program logics, model checking, etc.)
68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)

Software:

z3; Yices; veriT
PDFBibTeX XMLCite
Full Text: DOI arXiv

References:

[1] Althaus, E.; Kruglov, E.; Weidenbach, C.; Ghilardi, S. (ed.); Sebastiani, R. (ed.), Superposition modulo linear arithmetic sup(la), No. 5749, 84-99 (2009), Berlin · Zbl 1193.03024
[2] Armando, A., Ranise, S., Rusinowitch, M.: A rewriting approach to satisfiability procedures. Inf. Comput. 183(2), 140-164 (2003) · Zbl 1054.68077 · doi:10.1016/S0890-5401(03)00020-8
[3] Armando, A., Bonacina, M.P., Ranise, S., Schulz, S.: New results on rewrite-based satisfiability procedures. ACM Trans. Comput. Log. 10(1), 129-179 (2009) · Zbl 1367.68243 · doi:10.1145/1459010.1459014
[4] Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998) · Zbl 0948.68098 · doi:10.1017/CBO9781139172752
[5] Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification. J. Log. Comput. 3(4), 217-247 (1994) · Zbl 0814.68117 · doi:10.1093/logcom/4.3.217
[6] Bachmair, L., Ganzinger, H., Waldmann, U.: Refutational theorem proving for hierarchic first-order theories. Appl. Algebra Eng. Commun. Comput. 5(3), 193-212 (1994) · Zbl 0797.03008 · doi:10.1007/BF01190829
[7] Baumgartner, P., Waldmann, U.: Hierarchic superposition with weak abstraction. Bonacina, 39-57 (2013) · Zbl 1381.03017
[8] Baumgartner, P.; Bax, J.; Waldmann, U.; Demri, S. (ed.); Kapur, D. (ed.); Weidenbach, C. (ed.), Finite quantification in hierarchic theorem proving, No. 8562, 152-167 (2014), Berlin · Zbl 1423.68407
[9] Bonacina, M.P. (ed.): Automated Deduction—CADE-24—24th International Conference on Automated Deduction, Lake Placid, NY, USA, June 9-14, 2013. Proceedings, Lecture Notes in Computer Science, vol. 7898. Springer, Berlin (2013) · Zbl 1264.68002
[10] Bouton, T.; Oliveira, DCB; Déharbe, D.; Fontaine, P.; Schmidt, RA (ed.), Verit: an open, trustable and efficient smt-solver (2009), Berlin
[11] Caferra, R., Leitsch, A., Peltier, N.: Automated Model Building, Applied Logic Series, vol. 31. Kluwer, Dordrecht (2004) · Zbl 1085.03009 · doi:10.1007/978-1-4020-2653-9
[12] De Kleer, J.: An improved incremental algorithm for generating prime implicates. In: Proceedings of the National Conference on Artificial Intelligence, pp. 780-780. Wiley, London (1992) · Zbl 0797.03008
[13] de Moura, LM; Bjørner, N.; Ramakrishnan, CR (ed.); Rehof, J. (ed.), Z3: an efficient SMT solver, No. 4963, 337-340 (2008), Berlin
[14] Dillig, I.; Dillig, T.; Aiken, A.; Cousot, R. (ed.); Martel, M. (ed.), Small formulas for large programs: on-line constraint simplification in scalable static analysis, No. 6337, 236-252 (2010), Berlin · Zbl 1306.68024
[15] Dillig, I.; Dillig, T.; McMillan, KL; Aiken, A.; Madhusudan, P. (ed.); Seshia, SA (ed.), Minimum satisfying assignments for SMT, No. 7358, 394-409 (2012), Berlin
[16] Dutertre, D., de Moura, L.: The YICES SMT-solver. In: SMT-COMP: Satisfiability Modulo Theories Competition. http://yices.csl.sri.com (2006)
[17] Echenim, M., Peltier, N.: A calculus for generating ground explanations. In: Proceedings of the International Joint Conference on Automated Reasoning (IJCAR’12), LNCS, vol. 7364, pp. 194-209. Springer, Berlin (2012) · Zbl 1358.68189
[18] Echenim, M., Peltier, N., Tourret, S.: An approach to abductive reasoning in equational logic. In: Proceedings of IJCAI’13 (International Conference on Artificial Intelligence), AAAI, pp. 3-9 (2013)
[19] Echenim, M., Peltier, N., Tourret, S.: A rewriting strategy to generate prime implicates in equational logic. In: Proceedings of the International Joint Conference on Automated Reasoning (IJCAR’14). Springer, Berlin (2014) · Zbl 1423.68412
[20] Henocque, L.: The prime normal form of boolean formulas. Technical report at http://laurent.henocque.com/oldsite/element/2002Henocque-PNF-ResearchReport/RRLSIS-02-002.pdf (2002) · Zbl 1306.68024
[21] Jackson, P., Pais, J.: Computing prime implicants. In: 10th International Conference on Automated Deduction, pp. 543-557. Springer, Berlin (1990) · Zbl 1509.03043
[22] Kean, A., Tsiknis, G.: An incremental method for generating prime implicants/implicates. J. Symb. Comput. 9(2), 185-206 (1990) · Zbl 0704.68100 · doi:10.1016/S0747-7171(08)80029-6
[23] Knill, E., Cox, P., Pietrzykowski, T.: Equality and abductive residua for horn clauses. Theor. Comput. Sci. 120, 1-44 (1992) · Zbl 0788.68133 · doi:10.1016/0304-3975(93)90243-M
[24] Leitsch, A.: The resolution calculus. In: Brauer, W., Rozenberg, G., Salomaa, A. (eds.) Texts in Theoretical Computer Science. Springer, Berlin (1997) · Zbl 0867.68095
[25] Lynch, C., Morawska, B.: Automatic decidability. In: Proceedings of 17th IEEE Symposium on Logic in Computer Science (LICS’2002), IEEE Computer Society, Copenhagen, Denmark, pp. 7-16 (2002)
[26] Lynch, C., Ranise, S., Ringeissen, C., Tran, D.K.: Automatic decidability and combinability. Inf. Comput. 209(7), 1026-1047 (2011) · Zbl 1216.68163 · doi:10.1016/j.ic.2011.03.005
[27] Marquis, P.; Jorrand, P. (ed.); Kelemen, J. (ed.), Extending abduction from propositional to first-order logic, No. 535, 141-155 (1991), Berlin · Zbl 0793.03007
[28] Matusiewicz, A., Murray, N., Rosenthal, E.: Prime implicate tries. In: Giese, M., Waaler, A. (eds.) Automated Reasoning with Analytic Tableaux and Related Methods, pp. 250-264 Springer, Oslo (2009) · Zbl 1260.68127
[29] Matusiewicz, A., Murray, N., Rosenthal, E.: Tri-based set operations and selective computation of prime implicates. In: Foundations of Intelligent Systems, pp. 203-213 (2011)
[30] Mayer, M.C., Pirri, F.: First order abduction via tableau and sequent calculi. Logic J. IGPL 1(1), 99-117 (1993) · Zbl 0807.03005 · doi:10.1093/jigpal/1.1.99
[31] McCarthy, J.: Computer programs for checking mathematical proofs. In: Recursive Function Theory, Proceedings of Symposia in Pure Mathematics, Volume 5, American Mathematical Society, Providence, Rhode Island, pp. 219-228 (1962) · Zbl 0143.40007
[32] Meir, O., Strichman, O.: Yet another decision procedure for equality logic. In: Proceedings of the 17th International Conference on Computer Aided Verification, CAV’05, pp. 307-320. Springer, Berlin (2005) · Zbl 1081.68627
[33] Nieuwenhuis, R.; Rubio, A.; Robinson, JA (ed.); Voronkov, A. (ed.), Paramodulation-based theorem proving, 371-443 (2001), Cambridge · Zbl 0997.03012 · doi:10.1016/B978-044450813-3/50009-6
[34] Simon, L., Del Val, A.: Efficient consequence finding. In: Proceedings of the 17th International Joint Conference on Artificial Intelligence, pp. 359-370 (2001)
[35] Sofronie-Stokkermans, V.; Giesl, J. (ed.); Hähnle, R. (ed.), Hierarchical reasoning for the verification of parametric systems, No. 6173, 171-187 (2010), Berlin · Zbl 1291.68269
[36] Sofronie-Stokkermans, V.: Hierarchical reasoning and model generation for the verification of parametric hybrid systems. Bonacina 360-376 (2013) · Zbl 1381.68181
[37] Tison, P.: Generalization of consensus theory and application to the minimization of boolean functions. Electron. Comput. IEEE Trans. 4, 446-456 (1967) · Zbl 0158.16102 · doi:10.1109/PGEC.1967.264648
[38] Tran, D.K., Ringeissen, C., Ranise, S., Kirchner, H.: Combination of convex theories: modularity, deduction completeness, and explanation. J. Symb. Comput. 45(2), 261-286 (2010) · Zbl 1192.68190 · doi:10.1016/j.jsc.2008.10.006
[39] Tushkanova, E., Ringeissen, C., Giorgetti, A., Kouchnarenko, O.: Automatic decidability: a schematic calculus for theories with counting operators. In: van Raamsdonk, F. (ed.) RTA, Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, LIPIcs, vol. 21, pp. 303-318 (2013) · Zbl 1356.68204
[40] Wernhard, C.; Fontaine, P. (ed.); Ringeissen, C. (ed.); Schmidt, R. (ed.), Abduction in logic programming as second-order quantifier elimination, No. 8152, 103-119 (2013), Berlin · Zbl 1397.68165 · doi:10.1007/978-3-642-40885-4_8
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.