×

zbMATH — the first resource for mathematics

Superposition for bounded domains. (English) Zbl 1383.03018
Bonacina, Maria Paola (ed.) et al., Automated reasoning and mathematics. Essays in memory of William W. McCune. Berlin: Springer (ISBN 978-3-642-36674-1/pbk). Lecture Notes in Computer Science 7788. Lecture Notes in Artificial Intelligence, 68-100 (2013).
Summary: Reasoning about bounded domains in resolution calculi is often painful. For explicit and small domains and formulas with a few variables, grounding can be a successful approach. This approach was in particular shown to be effective by Bill McCune. For larger domains or larger formula sets with many variables, there is not much known. In particular, despite general decidability, superposition implementations that can meanwhile deal with large formula sets typically will not necessarily terminate. We start from the observation that lifting can be done more economically here: A variable does not stand anymore for every ground term, but just for the finitely many domain representatives. Thanks to this observation, the inference rules of superposition can drastically be restricted, and redundancy becomes effective. We present one calculus configuration which constitutes a decision procedure for satisfiability modulo the cardinality bound, and hence decides the Bernays-Schönfinkel class as a simple consequence. Finally, our approach also applies to bounded sorts in combination with arbitrary other, potentially infinite sorts in the framework of soft sorts. This frequent combination – which we recently explored in a combination of Spass and Isabelle – is an important motivation of our study.
For the entire collection see [Zbl 1259.68002].

MSC:
03B35 Mechanization of proofs and logical operations
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
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, vol. 5749, pp. 84–99. Springer, Heidelberg (2009) · Zbl 1193.03024
[2] Armando, A., Ranise, S., Rusinowitch, M.: Uniform Derivation of Decision Procedures by Superposition. In: Fribourg, L. (ed.) CSL 2001. LNCS, vol. 2142, pp. 513–527. Springer, Heidelberg (2001) · Zbl 1005.03012
[3] Armando, A., Bonacina, M.P., Ranise, S., Schulz, S.: New results on rewrite-based satisfiability procedures. ACM Transactions on Computational Logic 10(1), 4:1–4:51 (2009) · Zbl 1367.68243
[4] Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification. Journal of Logic and Computation 4(3), 217–247 (1994) · Zbl 0814.68117
[5] 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
[6] Baumgartner, P., Fuchs, A., de Nivelle, H., Tinelli, C.: Computing finite models by reduction to function-free clause logic. In: Ahrendt, W., Baumgartner, P., de Nivelle, H. (eds.) Proceedings of the Third Workshop on Disproving, pp. 82–99 (2006) · Zbl 1171.68040
[7] Baumgartner, P., Furbach, U., Pelzer, B.: The hyper tableaux calculus with equality and an application to finite model computation. Journal of Logic and Computation 20(1), 77–109 (2010) · Zbl 1193.03025
[8] Baumgartner, P., Schmidt, R.A.: Blocking and Other Enhancements for Bottom-Up Model Generation Methods. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 125–139. Springer, Heidelberg (2006) · Zbl 1222.68357
[9] Bernays, P., Schönfinkel, M.: Zum Entscheidungsproblem der mathematischen Logik. Mathematische Annalen 99, 342–372 (1928) · JFM 54.0056.05
[10] Blanchette, J.C., Popescu, A., Wand, D., Weidenbach, C.: More SPASS with Isabelle–Superposition with Hard Sorts and Configurable Simplification. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol. 7406, pp. 345–360. Springer, Heidelberg (2012), http://www4.in.tum.de/ blanchet/more-spass.pdf · Zbl 1360.68742
[11] Bonacina, M.P., Ghilardi, S., Nicolini, E., Ranise, S., Zucchelli, D.: Decidability and Undecidability Results for Nelson-Oppen and Rewrite-Based Decision Procedures. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 513–527. Springer, Heidelberg (2006) · Zbl 1222.03011
[12] Bonacina, M.P., Lynch, C., Mendonça de Moura, L.: On deciding satisfiability by theorem proving with speculative inferences. Journal of Automated Reasoning 47(2), 161–189 (2011) · Zbl 1243.68265
[13] Claessen, K., Sörensson, N.: New techniques that improve MACE-style finite model finding. In: Baumgartner, P., Fermueller, C. (eds.) Proceedings of the Workshop on Model Computation (2003)
[14] de Nivelle, H., Meng, J.: Geometric Resolution: A Proof Procedure Based on Finite Model Search. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 303–317. Springer, Heidelberg (2006) · Zbl 1222.68378
[15] Dershowitz, N.: A Maximal-Literal Unit Strategy for Horn Clauses. In: Okada, M., Kaplan, S. (eds.) CTRS 1990. LNCS, vol. 516, pp. 14–25. Springer, Heidelberg (1991)
[16] Fietzke, A., Weidenbach, C.: Labelled splitting. Annals of Mathematics and Artificial Intellelligence 55(1-2), 3–34 (2009) · Zbl 1192.68628
[17] Fietzke, A., Weidenbach, C.: Superposition as a decision procedure for timed automata. In: Ratschan, S. (ed.) MACIS 2011: Fourth International Conference on Mathematical Aspects of Computer and Information Sciences, pp. 52–62 (2011); Journal version to appear in the Journal of Mathematics in Computer Science · Zbl 1262.68159
[18] Fontaine, P., Merz, S., Weidenbach, C.: Combination of Disjoint Theories: Beyond Decidability. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol. 7364, pp. 256–270. Springer, Heidelberg (2012) · Zbl 1358.68253
[19] Ganzinger, H., Meyer, C., Weidenbach, C.: Soft Typing for Ordered Resolution. In: McCune, W. (ed.) CADE 1997. LNCS, vol. 1249, pp. 321–335. Springer, Heidelberg (1997)
[20] Hillenbrand, T., Topic, D., Weidenbach, C.: Sudokus as logical puzzles. In: Ahrendt, W., Baumgartner, P., de Nivelle, H. (eds.) Proceedings of the Third Workshop on Disproving, pp. 2–12 (2006)
[21] Hillenbrand, T., Weidenbach, C.: Superposition for finite domains. Research Report MPI-I-2007-RG1-002, Max-Planck-Institut für Informatik, Saarbrücken (2007), http://www.mpi-inf.mpg.de/ hillen/documents/HW07.ps
[22] Kamin, S., Levy, J.-J.: Attempts for generalizing the recursive path orderings. University of Illinois, Department of Computer Science. Unpublished note (1980), Available electronically from http://perso.ens-lyon.fr/pierre.lescanne/not_accessible.html
[23] Kirchner, H., Ranise, S., Ringeissen, C., Tran, D.-K.: On Superposition-Based Satisfiability Procedures and Their Combination. In: Van Hung, D., Wirsing, M. (eds.) ICTAC 2005. LNCS, vol. 3722, pp. 594–608. Springer, Heidelberg (2005) · Zbl 1169.68509
[24] Manthey, R., Bry, F.: Satchmo: A Theorem Prover Implemented in Prolog. In: Lusk, E., Overbeek, R. (eds.) CADE 1988. LNCS, vol. 310, pp. 415–434. Springer, Heidelberg (1988) · Zbl 0668.68104
[25] McCune, W.: Mace4 reference manual and guide. Technical Report ANL/MCS-TM-264, Argonne National Laboratory (2003)
[26] McCune, W.: Prover9 and mace4 (2005-2010), http://www.cs.unm.edu/ ccune/prover9/
[27] McCune, W.: Otter 3.3 reference manual. CoRR, cs.SC/0310056 (2003)
[28] Minsky, M.L.: Computation: Finite and Infinite Machines. Automatic Computation. Prentice-Hall (1967) · Zbl 0195.02402
[29] Nieuwenhuis, R., Rubio, A.: Paramodulation-based theorem proving. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. I, ch. 7, pp. 371–443. Elsevier (2001) · Zbl 0997.03012
[30] Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: From an abstract Davis–Putnam–Logemann–Loveland procedure to DPLL(T). Journal of the ACM 53, 937–977 (2006) · Zbl 1326.68164
[31] Paulson, L.C., Blanchette, J.C.: Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers. In: Sutcliffe, G., Ternovska, E., Schulz, S. (eds.) Proceedings of the 8th International Workshop on the Implementation of Logics (2010)
[32] Navarro, J.A., Voronkov, A.: Proof Systems for Effectively Propositional Logic. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 426–440. Springer, Heidelberg (2008) · Zbl 1165.03318
[33] Schulz, S., Bonacina, M.P.: On Handling Distinct Objects in the Superposition Calculus. In: Konev, B., Schulz, S. (eds.) Proc. of the 5th International Workshop on the Implementation of Logics, Montevideo, Uruguay, pp. 66–77 (2005)
[34] Slaney, J.: FINDER: Finite Domain Enumerator. In: Bundy, A. (ed.) CADE 1994. LNCS, vol. 814, pp. 798–801. Springer, Heidelberg (1994)
[35] Suda, M., Weidenbach, C., Wischnewski, P.: On the Saturation of YAGO. In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS, vol. 6173, pp. 441–456. Springer, Heidelberg (2010) · Zbl 1291.68372
[36] Weidenbach, C.: Combining superposition, sorts and splitting. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. II, ch. 27, pp. 1965–2012. Elsevier (2001) · Zbl 1011.68129
[37] Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: SPASS Version 3.5. In: Schmidt, R.A. (ed.) CADE 2009. LNCS, vol. 5663, pp. 140–145. Springer, Heidelberg (2009) · Zbl 05587933
[38] Wenzel, M., Paulson, L.C., Nipkow, T.: The Isabelle Framework. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 33–38. Springer, Heidelberg (2008) · Zbl 1165.68478
[39] Zhang, J., Zhang, H.: SEM: a system for enumerating models. In: Proceedings of the 14th International Joint Conference on Artificial Intelligence, vol. 1, pp. 298–303. Morgan Kaufmann (1995)
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.