Abstract
The hierarchic superposition calculus over a theory T, called SUP(T), enables sound reasoning on the hierarchic combination of a theory T with full first-order logic, FOL(T). If a FOL(T) clause set enjoys a sufficient completeness criterion, the calculus is even complete. Clause sets over the ground fragment of FOL(T) are not sufficiently complete, in general. In this paper we show that any clause set over the ground FOL(T) fragment can be transformed into a sufficiently complete one, and prove that SUP(T) terminates on the transformed clause set, hence constitutes a decision procedure provided the existential fragment of the theory T is decidable. Thanks to the hierarchic design of SUP(T), the decidability result can be extended beyond the ground case. We show SUP(T) is a decision procedure for the non-ground FOL fragment plus a theory T, if every non-constant function symbol from the underlying FOL signature ranges into the sort of the theory T, and every term of the theory sort is ground. Examples for T are in particular decidable fragments of arithmetic.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Althaus, E., Kruglov, E., Weidenbach, C.: Superposition modulo linear arithmetic SUP(LA). In: Ghilardi, S., Sebastiani, R. (eds.) Frontiers of Combining Systems: 7th International Symposium, FroCoS 2009, volume 5749 of Lecture Notes in Artificial Intelligence, pp. 84–99, Trento, Italy, September , Springer, Berlin (2009)
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)
Armando A., Ranise S., Rusinowitch M.: A rewriting approach to satisfiability procedures. Inform. Comput. 183(2), 140–164 (2003)
Baader F., Nipkow T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)
Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification. J. Logic Comput. 4(3):217–247, 1994. Revised version of Max-Planck-Institut für Informatik technical report, MPI-I-91-208 (1991)
Bachmair, L., Ganzinger, H., Waldmann, U.: Superposition with simplification as a decision procedure for the monadic class with equality. In: Gottlob, G., Leitsch, A., Mundici, D. (eds.) Computational Logic and Proof Theory, Third Kurt Gödel Colloquium, volume 713 of LNCS, pp. 83–96. Springer, August (1993)
Bachmair L., Ganzinger H., Waldmann U.: Refutational theorem proving for hierarchic first-order theories. AAECC 5(3/4), 193–212 (1994)
Baumgartner P., Fuchs A., Tinelli C.: ME(LIA)—model evolution with linear integer arithmetic constraints. In: LPAR 2008, volume 5330 of LNCS, pp. 258–273. Springer (2008)
Bonacina M.P., Lynch C., de Moura L.M.: On deciding satisfiability by theorem proving with speculative inferences. J. Autom. Reason. 47(2), 161–189 (2011)
Dershowitz N.: Orderings for term-rewriting systems. Theor. Comput. Sci. 17, 279–301 (1982)
Dershowitz N., Manna Z.: Proving termination with multiset orderings. Commun. ACM. 22(8), 465–476 (1979)
Eggers, A., Kruglov, E., Scheibler, K., Kupferschmid, S., Teige, T., Weidenbach, C.: SUP(NLA)—combining superposition and non-linear arithmetic. In: Sofronie-Stokkermans, V., Tinelli, C. (eds.) Frontiers of Combining Systems, 8th International Symposium, FroCos 2011, Lecture Notes in Computer Science. Springer, Berlin (2011)
Fietzke, A., Hermanns, H., Weidenbach C.: Superposition-based analysis of first-order probabilistic timed automata. In: Proceedings of the 17th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR’10, pp. 302–316, Berlin, Heidelberg, Springer Verlag (2010)
Fietzke, A., Kruglov, E.,Weidenbach C.: Automatic generation of inductive invariants by SUP(LA). Research Report MPI-I-2012-RG1-002, Max-Planck Institute for Informatics, Saarbrücken, Germany, March (2012)
Fietzke, A., Kruglov, E., Weidenbach C.: Automatic generation of invariants for circular derivations in SUP(LA). In: Proceedings of the 18th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, volume 7180 of Lecture Notes in Computer Science, pp. 197–211. Springer, Berlin, March (2012)
Fietzke, A., Weidenbach, C.: Superposition as a decision procedure for timed automata. In: Ratschan, S. (ed.) Fourth International Conference on Mathematical Aspects of Computer and Information Sciences (MACIS 2011), Beijing, China, 2011. Internal Conference Proceedings (2011)
Ganzinger H., Sofronie-Stokkermans V., Waldmann U.: Modular proof systems for partial functions with Evans equality. Inform. Comput. 204(10), 1453–1492 (2006)
Hillenbrand, T., Weidenbach, C.: Superposition for finite domains. Research Report MPI-I-2007-RG1-002, Max-Planck Institute for Informatics, Saarbruecken, Germany, April (2007)
Hustadt U., Schmidt R.A., Georgieva L.: A survey of decidable first-order fragments and description logics. J. Relat. Methods Comput. Sci. 1, 251–276 (2004)
Ihlemann, C., Jacobs, S., Sofronie-Stokkermans V.: On local reasoning in verification. In: Ramakrishnan, C.R., Rehof, J. (eds.) Proceedings of TACAS 2008, volume 4963 of LNCS, pp. 265–281. Springer, Berlin (2008)
Jacquemard, F., Meyer, C., Weidenbach C.: Unification in extensions of shallow equational theories. In: Nipkow, T. (ed.) Rewriting Techniques and Applications, 9th International Conference, RTA-98, volume 1379 of LNCS, pp. 76–90. Springer, Berlin (1998)
Korovin, K., Voronkov A.: Integrating linear arithmetic into superposition calculus. In Duparc, J., Henzinger, T.A. (eds.) CSL 2007, volume 4646 of LNCS, pp. 223–237. Springer, Berlin (2007)
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, pp. 937–977, November (2006)
Sebastiani R.: Lazy satisability modulo theories. JSAT 3(3–4), 141–224 (2007)
Suchanek, F.M., Kasneci,G., Weikum G.: Yago: a core of semantic knowledge. In: Proceedings of the 16th international conference on World Wide Web, WWW ’07, pp. 697–706, New York, NY, USA, ACM (2007)
Suda, M., Weidenbach, C., Wischnewski P.: On the saturation of yago. In: Proceedings of the 5th international conference on Automated Reasoning, IJCAR’10, pp. 441–456, Berlin, Heidelberg, Springer, Berlin (2010)
Waldmann, U.: Superposition and chaining for totally ordered divisible abelian groups. In Goré, R., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001, volume 2083 of LNAI, pp. 226–241. Springer, Berlin (2001)
Weidenbach, C.: Combining superposition, sorts and splitting. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol 2, chapter 27, pp. 1965–2012. Elsevier, Amsterdam (2001)
Weidenbach, C., Wischnewski, P.: Satisfiability checking and query answering for large ontologies. In: Fontaine, P., Schmidt, R., Schulz, S. (eds.) PAAR-2012: IJCAR’12 Workshop on Practical Aspects of Automated Reasoning, pp. 163–177 (2012)
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Kruglov, E., Weidenbach, C. Superposition Decides the First-Order Logic Fragment Over Ground Theories. Math.Comput.Sci. 6, 427–456 (2012). https://doi.org/10.1007/s11786-012-0135-4
Received:
Revised:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s11786-012-0135-4