×

zbMATH — the first resource for mathematics

On first-order model-based reasoning. (English) Zbl 1322.03013
Martí-Oliet, Narciso (ed.) et al., Logic, rewriting, and concurrency. Essays dedicated to José Meseguer on the occasion of his 65th birthday. Cham: Springer (ISBN 978-3-319-23164-8/pbk; 978-3-319-23165-5/ebook). Lecture Notes in Computer Science 9200, 181-204 (2015).
Summary: Reasoning semantically in first-order logic is notoriously a challenge. This paper surveys a selection of semantically-guided or model-based methods that aim at meeting aspects of this challenge. For first-order logic we touch upon resolution-based methods, tableaux-based methods, DPLL-inspired methods, and we give a preview of a new method called SGGS, for Semantically-Guided Goal-Sensitive reasoning. For first-order theories we highlight hierarchical and locality-based methods, concluding with the recent Model-Constructing satisfiability calculus.
For the entire collection see [Zbl 1319.68011].

MSC:
03B35 Mechanization of proofs and logical operations
03B10 Classical first-order logic
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Althaus, E., Kruglov, E., Weidenbach, C.: Superposition modulo linear arithmetic SUP(LA). In: Ghilardi, S., Sebastiani, R. (eds.) FroCoS 2009. LNCS (LNAI), vol. 5749, pp. 84–99. Springer, Heidelberg (2009) · Zbl 1193.03024 · doi:10.1007/978-3-642-04222-5_5
[2] Aravindan, C., Baumgartner, P.: Theorem proving techniques for view deletion in databases. J. Symbolic Comput. 29(2), 119–148 (2000) · Zbl 0967.68149 · doi:10.1006/jsco.1999.0358
[3] Arthan, R., Oliva, P.: (Dual) Hoops have unique halving. In: Bonacina, M.P., Stickel, M.E. (eds.) Automated Reasoning and Mathematics: Essays in Memory of William W. McCune. LNCS (LNAI), vol. 7788, pp. 165–180. Springer, Heidelberg (2013) · Zbl 1383.68068 · doi:10.1007/978-3-642-36675-8_9
[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] Bachmair, L., Ganzinger, H.: Ordered chaining calculi for first-order theories of transitive relations. J. ACM 45(6), 1007–1049 (1998) · Zbl 1065.68615 · doi:10.1145/293347.293352
[6] Bachmair, L., Ganzinger, H., Waldmann, U.: Refutational theorem proving for hierarchic first-order theories. Appl. Algebra Eng. Commun. Comput. 5, 193–212 (1994) · Zbl 0797.03008 · doi:10.1007/BF01190829
[7] Barrett, C., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Biere, A., Heule, M., Van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, chap. 26, pp. 825–886. IOS Press, Amsterdam (2009)
[8] Baumgartner, P., Fröhlich, P., Furbach, U., Nejdl, W.: Semantically guided theorem proving for diagnosis applications. In: Proceedings of IJCAI-16, vol. 1, pp. 460–465 (1997)
[9] Baumgartner, P., Fuchs, A., Tinelli, C.: Implementing the model evolution calculus. Int. J. Artif. Intell. Tools 15(1), 21–52 (2006) · Zbl 05421296 · doi:10.1142/S0218213006002552
[10] Baumgartner, P., Furbach, U., Niemelä, I.: Hyper tableaux. In: Alferes, J.J., Moniz Pereira, L., Orłowska, E. (eds.) JELIA 1996. LNCS (LNAI), vol. 1126, pp. 1–17. Springer, Heidelberg (1996) · doi:10.1007/3-540-61630-6_1
[11] Baumgartner, P., Furbach, U., Pelzer, B.: The hyper tableaux calculus with equality and an application to finite model computation. J. Logic Comput. 20(1), 77–109 (2008) · Zbl 1193.03025 · doi:10.1093/logcom/exn061
[12] Baumgartner, P., Pelzer, B., Tinelli, C.: Model evolution calculus with equality - revised and implemented. J. Symbolic Comput. 47(9), 1011–1045 (2012) · Zbl 1258.03020 · doi:10.1016/j.jsc.2011.12.031
[13] Baumgartner, P., Tinelli, C.: The model evolution calculus as a first-order DPLL method. Artif. Intell. 172(4–5), 591–632 (2008) · Zbl 1182.03034 · doi:10.1016/j.artint.2007.09.005
[14] Baumgartner, P., Waldmann, U.: Superposition and model evolution combined. In: Schmidt, R.A. (ed.) CADE-22. LNCS (LNAI), vol. 5663, pp. 17–34. Springer, Heidelberg (2009) · Zbl 1237.03010 · doi:10.1007/978-3-642-02959-2_2
[15] Baumgartner, P., Waldmann, U.: Hierarchic superposition with weak abstraction. In: Bonacina, M.P. (ed.) CADE-24. LNCS (LNAI), vol. 7898, pp. 39–57. Springer, Heidelberg (2013) · Zbl 1381.03017 · doi:10.1007/978-3-642-38574-2_3
[16] Bender, M., Pelzer, B., Schon, C.: System description: E-KRHyper 1.4 – Extensions for unique names and description logic. In: Bonacina, M.P. (ed.) CADE-24. LNCS (LNAI), vol. 7898, pp. 126–134. Springer, Heidelberg (2013) · Zbl 1381.68258 · doi:10.1007/978-3-642-38574-2_8
[17] Bibel, W., Schmitt, P.H. (eds.): Automated Deduction - A Basis for Applications (in 2 volumes). Kluwer Academic Publishers, Dordrecht (1998) · Zbl 0954.00010
[18] Bonacina, M.P.: A taxonomy of theorem-proving strategies. In: Veloso, M.M., Wooldridge, M.J. (eds.) Artificial Intelligence Today - Recent Trends and Developments. LNCS (LNAI), vol. 1600, pp. 43–84. Springer, Heidelberg (1999) · Zbl 0984.03011 · doi:10.1007/3-540-48317-9_3
[19] Bonacina, M.P.: On theorem proving for program checking - Historical perspective and recent developments. In: Fernández, M. (eds.): Proceedings of PPDP-12, pp. 1–11. ACM Press (2010)
[20] Bonacina, M.P., Echenim, M.: Theory decision by decomposition. J. Symbolic Comput. 45(2), 229–260 (2010) · Zbl 1192.68626 · doi:10.1016/j.jsc.2008.10.008
[21] Bonacina, M.P., Hsiang, J.: Towards a foundation of completion procedures as semidecision procedures. Theoret. Comput. Sci. 146, 199–242 (1995) · Zbl 0873.68107 · doi:10.1016/0304-3975(94)00187-N
[22] Bonacina, M.P., Hsiang, J.: On semantic resolution with lemmaizing and contraction and a formal treatment of caching. New Gener. Comput. 16(2), 163–200 (1998) · doi:10.1007/BF03037315
[23] Bonacina, M.P., Johansson, M.: Interpolation of ground proofs in automated deduction: a survey. J. Autom. Reasoning 54(4), 353–390 (2015) · Zbl 1356.68179 · doi:10.1007/s10817-015-9325-5
[24] Bonacina, M.P., Johansson, M.: On interpolation in automated theorem proving. J. Autom. Reasoning 54(1), 69–97 (2015) · Zbl 1315.03018 · doi:10.1007/s10817-014-9314-0
[25] Bonacina, M.P., Lynch, C.A., de Moura, L.: On deciding satisfiability by theorem proving with speculative inferences. J. Autom. Reasoning 47(2), 161–189 (2011) · Zbl 1243.68265 · doi:10.1007/s10817-010-9213-y
[26] Bonacina, M.P., Plaisted, D.A.: Constraint manipulation in SGGS. In: Kutsia, T., Ringeissen, C. (eds.) Proceedings of UNIF-28, RISC Technical Reports, pp. 47–54. Johannes Kepler Universität, Linz (2014)
[27] Bonacina, M.P., Plaisted, D.A.: SGGS theorem proving: an exposition. In: Schulz, S., de Moura, L., Konev, B. (eds.) Proceedings of PAAR-4, EasyChair Proceedings in Computing (EPiC), pp. 25–38 (2015)
[28] Bonacina, M.P., Plaisted, D.A.: Semantically guided goal-sensitive reasoning: inference system and completeness (2015, in preparation) · Zbl 1356.68180
[29] Bonacina, M.P., Plaisted, D.A.: Semantically-guided goal-sensitive reasoning: model representation. J. Autom. Reasoning 55(1), 1–29 (2015). doi: 10.1007/s10817-015-9334-4 · Zbl 1356.68180 · doi:10.1007/s10817-015-9334-4
[30] Boy de la Tour, T., Echenim, M.: Permutative rewriting and unification. Inf. Comput. 205(4), 624–650 (2007) · Zbl 1112.68072 · doi:10.1016/j.ic.2006.11.001
[31] Chang, C.-L., Lee, R.C.-T.: Symbolic logic and mechanical theorem proving. Academic Press, New York (1973) · Zbl 0263.68046
[32] 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
[33] Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM 7, 201–215 (1960) · Zbl 0212.34203 · doi:10.1145/321033.321034
[34] de Moura, L., Bjørner, N.: Satisfiability modulo theories: introduction and applications. Commun. ACM 54(9), 69–77 (2011) · doi:10.1145/1995376.1995394
[35] de Moura, L., Jovanović, D.: A model-constructing satisfiability calculus. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 1–12. Springer, Heidelberg (2013) · Zbl 1426.68251 · doi:10.1007/978-3-642-35873-9_1
[36] Dershowitz, N., Jouannaud, J.-P.: Rewrite systems. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol. B, pp. 243–320. Elsevier, Amsterdam (1990) · Zbl 0900.68283
[37] Escobar, S., Meseguer, J., Sasse, R.: Variant narrowing and equational unification. Electron. Notes Theoret. Comput. Sci. 238, 103–119 (2009) · Zbl 1347.68194 · doi:10.1016/j.entcs.2009.05.015
[38] Fitelson, B.: Gibbard’s collapse theorem for the indicative conditional: an axiomatic approach. In: Bonacina, M.P., Stickel, M.E. (eds.) Automated Reasoning and Mathematics: Essays in Memory of William W. McCune. LNCS (LNAI), vol. 7788, pp. 181–188. Springer, Heidelberg (2013) · Zbl 1383.03011 · doi:10.1007/978-3-642-36675-8_10
[39] Furbach, U., Schon, C.: Semantically guided evolution of \[ {\mathcal S}{\mathcal H}{\mathcal I} \] S H I ABoxes. In: Galmiche, D., Larchey-Wendling, D. (eds.) TABLEAUX 2013. LNCS (LNAI), vol. 8123, pp. 17–34. Springer, Heidelbeg (2013)
[40] Gallier, J.H., Snyder, W.: Designing unification procedures using transformations: a survey. EATCS Bull. 40, 273–326 (1990) · Zbl 0744.68112
[41] Ganzinger, H., Sofronie-Stokkermans, V., Waldmann, U.: Modular proof systems for partial functions with Evans equality. Inf. Comput. 240(10), 1453–1492 (2006) · Zbl 1103.68112 · doi:10.1016/j.ic.2005.10.002
[42] Ganzinger, H., Waldmann, U.: Theorem proving in cancellative abelian monoids. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE-13. LNCS, vol. 1104, pp. 388–402. Springer, Heidelberg (1996) · doi:10.1007/3-540-61511-3_102
[43] Goguen, J., Meseguer, J.: Order-sorted unification. J. Symbolic Comput. 8(4), 383–413 (1989) · Zbl 0691.03002 · doi:10.1016/S0747-7171(89)80036-7
[44] Goguen, J., Meseguer, J.: Order-sorted algebra I: equational deduction for multiple inheritance, overloading, exceptions and partial operations. Theoret. Comput. Sci. 105(2), 217–273 (1992) · Zbl 0778.68056 · doi:10.1016/0304-3975(92)90302-V
[45] Hendrix, J., Clavel, M., Meseguer, J.: A sufficient completeness reasoning tool for partial specifications. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 165–174. Springer, Heidelberg (2005) · Zbl 1078.68668 · doi:10.1007/978-3-540-32033-3_13
[46] Hendrix, J., Meseguer, J.: Order-sorted equational unification revisited. Electron. Notes Theoret. Comput. Sci. 290(3), 37–50 (2012) · Zbl 1291.68220 · doi:10.1016/j.entcs.2012.11.010
[47] Hendrix, J., Meseguer, J., Ohsaki, H.: A sufficient completeness checker for linear order-sorted specifications modulo axioms. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 151–155. Springer, Heidelberg (2006) · Zbl 05528283 · doi:10.1007/11814771_14
[48] Hsiang, J., Rusinowitch, M.: Proving refutational completeness of theorem proving strategies: the transfinite semantic tree method. J. ACM 38(3), 559–587 (1991) · Zbl 0799.68170 · doi:10.1145/116825.116833
[49] Hsiang, J., Rusinowitch, M., Sakai, K.: Complete inference rules for the cancellation laws. In: Proceedings of IJCAI-10, pp. 990–992 (1987)
[50] Ihlemann, C., Jacobs, S., Sofronie-Stokkermans, V.: On local reasoning in verification. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 265–281. Springer, Heidelberg (2008) · Zbl 1134.68410 · doi:10.1007/978-3-540-78800-3_19
[51] Ihlemann, C., Sofronie-Stokkermans, V.: On hierarchical reasoning in combinations of theories. In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS (LNAI), vol. 6173, pp. 30–45. Springer, Heidelberg (2010) · Zbl 1291.03018 · doi:10.1007/978-3-642-14203-1_4
[52] Marques-Silva, J.P., Sakallah, K.A.: GRASP: a new search algorithm for satisfiability. In: Proceedings of ICCAD 1996, pp. 220–227 (1997)
[53] Jouannaud, J.-P., Kirchner, C.: Solving equations in abstract algebras: a rule-based survey of unification. In: Lassez, J.-L., Plotkin, G. (eds.) Computational Logic - Essays in Honor of Alan Robinson, pp. 257–321. MIT Press, Cambridge (1991)
[54] Jouannaud, J.-P., Kirchner, H.: Completion of a set of rules modulo a set of equations. SIAM J. Comput. 15(4), 1155–1194 (1986) · Zbl 0665.03005 · doi:10.1137/0215084
[55] Jovanović, D., Barrett, C., de Moura, L.: The design and implementation of the model-constructing satisfiability calculus. In: Jobstman, B., Ray, S. (eds.) Proceedings of FMCAD-13. ACM and IEEE (2013) · doi:10.1109/FMCAD.2013.7027033
[56] Kapur, D.: An automated tool for analyzing completeness of equational specifications. In: Proceedings of ISSTA-94, pp. 28–43. ACM (1994) · doi:10.1145/186258.186496
[57] Kapur, D., Narendran, P., Rosenkrantz, D.J., Zhang, H.: Sufficient-completeness, ground-reducibility and their complexity. Acta Informatica 28(4), 311–350 (1991) · Zbl 0721.68032 · doi:10.1007/BF01893885
[58] Lee, S.-J., Plaisted, D.A.: Eliminating duplication with the hyperlinking strategy. J. Autom. Reasoning 9, 25–42 (1992) · Zbl 0784.68077
[59] Lifschitz, V., Morgenstern, L., Plaisted, D.A.: Knowledge representation and classical logic. In: van Harmelen, F., Lifschitz, V., Porter, B. (eds.) Handbook of Knowledge Representation, vol. 1, pp. 3–88. Elsevier, Amsterdam (2008) · doi:10.1016/S1574-6526(07)03001-5
[60] Malik, S., Zhang, L.: Boolean satisfiability: from theoretical hardness to practical success. Commun. ACM 52(8), 76–82 (2009) · Zbl 05747903 · doi:10.1145/1536616.1536637
[61] McCune, W.W.: OTTER 3.3 reference manual. Technical Report ANL/MCS-TM-263, MCS Division, Argonne National Laboratory, Argonne (2003)
[62] Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: Blaauw, D., Lavagno, L. (eds.) Proceedings of DAC-39, pp. 530–535 (2001) · doi:10.1145/378239.379017
[63] Nelson, G.: Combining satisfiability procedures by equality sharing. In: Bledsoe, W.W., Loveland, D.W. (eds.) Automatic Theorem Proving: After 25 Years, pp. 201–211. American Mathematical Society, Providence (1983)
[64] Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Trans. Program. Lang. 1(2), 245–257 (1979) · Zbl 0452.68013 · doi:10.1145/357073.357079
[65] Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: from an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). J. ACM 53(6), 937–977 (2006) · Zbl 1326.68164 · doi:10.1145/1217856.1217859
[66] Peterson, G.E., Stickel, M.E.: Complete sets of reductions for some equational theories. J. ACM 28(2), 233–264 (1981) · Zbl 0479.68092 · doi:10.1145/322248.322251
[67] Plaisted, D.A.: Mechanical theorem proving. In: Banerji, R.B. (ed.) Formal Techniques in Artificial Intelligence, pp. 269–320. Elsevier, Amsterdam (1990) · Zbl 0704.68095
[68] Plaisted, D.A.: Equational reasoning and term rewriting systems. In: Gabbay, D.M., Hogger, C.J., Robinson, J.A. (eds.) Handbook of Logic in Artificial Intelligence and Logic Programming. Vol. I: Logical Foundations, pp. 273–364. Oxford University Press, Oxford (1993)
[69] Plaisted, D.A.: Automated theorem proving. Wiley Interdisciplinary Reviews: Cognitive Science 5(2), 115–128 (2014)
[70] Plaisted, D.A., Zhu, Y.: The Efficiency of Theorem Proving Strategies. Friedrich Vieweg & Sohns, Braunschweig (1997) · Zbl 0881.68106 · doi:10.1007/978-3-322-93862-6
[71] Plaisted, D.A., Zhu, Y.: Ordered semantic hyper linking. J. Autom. Reasoning 25, 167–217 (2000) · Zbl 0959.68115 · doi:10.1023/A:1006376231563
[72] Plotkin, G.: Building in equational theories. Mach. Intell. 7, 73–90 (1972) · Zbl 0262.68036
[73] Robinson, G.A., Wos, L.: Paramodulation and theorem proving in first order theories with equality. Mach. Intell. 4, 135–150 (1969) · Zbl 0219.68047
[74] Robinson, J.A.: Automatic deduction with hyper-resolution. Int. J. Comput. Math. 1, 227–234 (1965) · Zbl 0158.26003
[75] 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
[76] Robinson, J.A., Voronkov, A. (eds.): Handbook of Automated Reasoning. Elsevier and MIT Press, Amsterdam (2001) · Zbl 0964.00020
[77] Rusinowitch, M.: Theorem-proving with resolution and superposition. J. Symbolic Comput. 11(1 & 2), 21–50 (1991) · Zbl 0723.68094 · doi:10.1016/S0747-7171(08)80131-9
[78] Shearer, R., Motik, B., Horrocks, I.: HermiT: a highly efficient OWL reasoner. In: Ruttenberg, A., Sattler, U., Dolbear, C. (eds.) Proceedings of OWLED-5, vol. 432 of CEUR (2008)
[79] Slagle, J.R.: Automatic theorem proving with renamable and semantic resolution. J. ACM 14(4), 687–697 (1967) · Zbl 0157.02405 · doi:10.1145/321420.321428
[80] Slaney, J., Lusk, E., McCune, W.: SCOTT: semantically constrained Otter system description. In: Bundy, A. (ed.) CADE-12. LNCS (LNAI), vol. 814, pp. 764–768. Springer, Heidelberg (1994) · doi:10.1007/3-540-58156-1_56
[81] Sofronie-Stokkermans, V.: Hierarchic reasoning in local theory extensions. In: Nieuwenhuis, R. (ed.) CADE-20. LNCS (LNAI), vol. 3632, pp. 219–234. Springer, Heidelberg (2005) · Zbl 1135.03330 · doi:10.1007/11532231_16
[82] Sofronie-Stokkermans, V.: Hierarchical and modular reasoning in complex theories: the case of local theory extensions. In: Konev, B., Wolter, F. (eds.) FroCos 2007. LNCS (LNAI), vol. 4720, pp. 47–71. Springer, Heidelberg (2007) · Zbl 1148.68469 · doi:10.1007/978-3-540-74621-8_3
[83] Sofronie-Stokkermans, V.: Interpolation in local theory extensions. Logical Methods in Computer Science, 4(4), 1–31, Paper 1 (2008) · Zbl 1170.03018
[84] Stuber, J.: Superposition theorem proving for abelian groups represented as integer modules. Theoret. Comput. Sci. 208(1–2), 149–177 (1998) · Zbl 0912.68187 · doi:10.1016/S0304-3975(98)00082-6
[85] Waldmann, U.: Superposition for divisible torsion-free abelian groups. In: Kirchner, C., Kirchner, H. (eds.) CADE-15. LNCS (LNAI), vol. 1421, pp. 144–159. Springer, Heidelberg (1998) · Zbl 0924.03026 · doi:10.1007/BFb0054257
[86] 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 · doi:10.1145/321296.321302
[87] Zhang, H., Zhang, J.: MACE4 and SEM: a comparison of finite model generators. In: Bonacina, M.P., Stickel, M.E. (eds.) Automated Reasoning and Mathematics: Essays in Memory of William W. McCune. LNCS (LNAI), vol. 7788, pp. 101–130. Springer, Heidelberg (2013) · Zbl 1383.68083 · doi:10.1007/978-3-642-36675-8_5
[88] Zhang, L., Malik, S.: The quest for efficient boolean satisfiability solvers. In: Voronkov, A. (ed.) CADE-18. LNCS (LNAI), vol. 2392, pp. 295–313. Springer, Heidelberg (2002) · Zbl 1072.68599 · doi:10.1007/3-540-45620-1_26
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.