{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,24]],"date-time":"2025-04-24T04:41:18Z","timestamp":1745469678546,"version":"3.40.4"},"reference-count":29,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2012,12,1]],"date-time":"2012-12-01T00:00:00Z","timestamp":1354320000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math.Comput.Sci."],"published-print":{"date-parts":[[2012,12]]},"DOI":"10.1007\/s11786-012-0135-4","type":"journal-article","created":{"date-parts":[[2012,12,18]],"date-time":"2012-12-18T12:38:33Z","timestamp":1355834313000},"page":"427-456","source":"Crossref","is-referenced-by-count":10,"title":["Superposition Decides the First-Order Logic Fragment Over Ground Theories"],"prefix":"10.1007","volume":"6","author":[{"given":"Evgeny","family":"Kruglov","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christoph","family":"Weidenbach","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2012,12,19]]},"reference":[{"key":"135_CR1","doi-asserted-by":"crossref","unstructured":"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\u201399, Trento, Italy, September , Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-04222-5_5"},{"issue":"1","key":"135_CR2","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1145\/1459010.1459014","volume":"10","author":"A. Armando","year":"2009","unstructured":"Armando A., Bonacina M.P., Ranise S., Schulz S.: New results on rewrite-based satisfiability procedures. ACM Trans. Comput. Log. 10(1), 129\u2013179 (2009)","journal-title":"ACM Trans. Comput. Log."},{"issue":"2","key":"135_CR3","doi-asserted-by":"crossref","first-page":"140","DOI":"10.1016\/S0890-5401(03)00020-8","volume":"183","author":"A. Armando","year":"2003","unstructured":"Armando A., Ranise S., Rusinowitch M.: A rewriting approach to satisfiability procedures. Inform. Comput. 183(2), 140\u2013164 (2003)","journal-title":"Inform. Comput."},{"key":"135_CR4","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139172752","volume-title":"Term Rewriting and All That","author":"F. Baader","year":"1998","unstructured":"Baader F., Nipkow T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)"},{"key":"135_CR5","doi-asserted-by":"crossref","unstructured":"Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification. J. Logic Comput. 4(3):217\u2013247, 1994. Revised version of Max-Planck-Institut f\u00fcr Informatik technical report, MPI-I-91-208 (1991)","DOI":"10.1093\/logcom\/4.3.217"},{"key":"135_CR6","doi-asserted-by":"crossref","unstructured":"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\u00f6del Colloquium, volume 713 of LNCS, pp. 83\u201396. Springer, August (1993)","DOI":"10.1007\/BFb0022557"},{"issue":"3\/4","key":"135_CR7","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1007\/BF01190829","volume":"5","author":"L. Bachmair","year":"1994","unstructured":"Bachmair L., Ganzinger H., Waldmann U.: Refutational theorem proving for hierarchic first-order theories. AAECC 5(3\/4), 193\u2013212 (1994)","journal-title":"AAECC"},{"key":"135_CR8","doi-asserted-by":"crossref","unstructured":"Baumgartner P., Fuchs A., Tinelli C.: ME(LIA)\u2014model evolution with linear integer arithmetic constraints. In: LPAR 2008, volume 5330 of LNCS, pp. 258\u2013273. Springer (2008)","DOI":"10.1007\/978-3-540-89439-1_19"},{"issue":"2","key":"135_CR9","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1007\/s10817-010-9213-y","volume":"47","author":"M.P. Bonacina","year":"2011","unstructured":"Bonacina M.P., Lynch C., de Moura L.M.: On deciding satisfiability by theorem proving with speculative inferences. J. Autom. Reason. 47(2), 161\u2013189 (2011)","journal-title":"J. Autom. Reason."},{"key":"135_CR10","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1016\/0304-3975(82)90026-3","volume":"17","author":"N. Dershowitz","year":"1982","unstructured":"Dershowitz N.: Orderings for term-rewriting systems. Theor. Comput. Sci. 17, 279\u2013301 (1982)","journal-title":"Theor. Comput. Sci."},{"issue":"8","key":"135_CR11","doi-asserted-by":"crossref","first-page":"465","DOI":"10.1145\/359138.359142","volume":"22","author":"N. Dershowitz","year":"1979","unstructured":"Dershowitz N., Manna Z.: Proving termination with multiset orderings. Commun. ACM. 22(8), 465\u2013476 (1979)","journal-title":"Commun. ACM."},{"key":"135_CR12","doi-asserted-by":"crossref","unstructured":"Eggers, A., Kruglov, E., Scheibler, K., Kupferschmid, S., Teige, T., Weidenbach, C.: SUP(NLA)\u2014combining 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)","DOI":"10.1007\/978-3-642-24364-6_9"},{"key":"135_CR13","doi-asserted-by":"crossref","unstructured":"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\u201910, pp. 302\u2013316, Berlin, Heidelberg, Springer Verlag (2010)","DOI":"10.1007\/978-3-642-16242-8_22"},{"key":"135_CR14","unstructured":"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\u00fccken, Germany, March (2012)"},{"key":"135_CR15","doi-asserted-by":"crossref","unstructured":"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\u2013211. Springer, Berlin, March (2012)","DOI":"10.1007\/978-3-642-28717-6_17"},{"key":"135_CR16","unstructured":"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)"},{"issue":"10","key":"135_CR17","doi-asserted-by":"crossref","first-page":"1453","DOI":"10.1016\/j.ic.2005.10.002","volume":"204","author":"H. Ganzinger","year":"2006","unstructured":"Ganzinger H., Sofronie-Stokkermans V., Waldmann U.: Modular proof systems for partial functions with Evans equality. Inform. Comput. 204(10), 1453\u20131492 (2006)","journal-title":"Inform. Comput."},{"key":"135_CR18","unstructured":"Hillenbrand, T., Weidenbach, C.: Superposition for finite domains. Research Report MPI-I-2007-RG1-002, Max-Planck Institute for Informatics, Saarbruecken, Germany, April (2007)"},{"key":"135_CR19","first-page":"251","volume":"1","author":"U. Hustadt","year":"2004","unstructured":"Hustadt U., Schmidt R.A., Georgieva L.: A survey of decidable first-order fragments and description logics. J. Relat. Methods Comput. Sci. 1, 251\u2013276 (2004)","journal-title":"J. Relat. Methods Comput. Sci."},{"key":"135_CR20","doi-asserted-by":"crossref","unstructured":"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\u2013281. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-78800-3_19"},{"key":"135_CR21","doi-asserted-by":"crossref","unstructured":"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\u201390. Springer, Berlin (1998)","DOI":"10.1007\/BFb0052362"},{"key":"135_CR22","doi-asserted-by":"crossref","unstructured":"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\u2013237. Springer, Berlin (2007)","DOI":"10.1007\/978-3-540-74915-8_19"},{"key":"135_CR23","doi-asserted-by":"crossref","unstructured":"Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving sat and sat modulo theories: from an abstract davis\u2013putnam\u2013logemann\u2013loveland procedure to dpll(t). J. ACM. 53, pp. 937\u2013977, November (2006)","DOI":"10.1145\/1217856.1217859"},{"issue":"3\u20134","key":"135_CR24","first-page":"141","volume":"3","author":"R. Sebastiani","year":"2007","unstructured":"Sebastiani R.: Lazy satisability modulo theories. JSAT 3(3\u20134), 141\u2013224 (2007)","journal-title":"JSAT"},{"key":"135_CR25","doi-asserted-by":"crossref","unstructured":"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 \u201907, pp. 697\u2013706, New York, NY, USA, ACM (2007)","DOI":"10.1145\/1242572.1242667"},{"key":"135_CR26","doi-asserted-by":"crossref","unstructured":"Suda, M., Weidenbach, C., Wischnewski P.: On the saturation of yago. In: Proceedings of the 5th international conference on Automated Reasoning, IJCAR\u201910, pp. 441\u2013456, Berlin, Heidelberg, Springer, Berlin (2010)","DOI":"10.1007\/978-3-642-14203-1_38"},{"key":"135_CR27","doi-asserted-by":"crossref","unstructured":"Waldmann, U.: Superposition and chaining for totally ordered divisible abelian groups. In Gor\u00e9, R., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001, volume 2083 of LNAI, pp. 226\u2013241. Springer, Berlin (2001)","DOI":"10.1007\/3-540-45744-5_17"},{"key":"135_CR28","doi-asserted-by":"crossref","unstructured":"Weidenbach, C.: Combining superposition, sorts and splitting. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol 2, chapter 27, pp. 1965\u20132012. Elsevier, Amsterdam (2001)","DOI":"10.1016\/B978-044450813-3\/50029-1"},{"key":"135_CR29","doi-asserted-by":"crossref","unstructured":"Weidenbach, C., Wischnewski, P.: Satisfiability checking and query answering for large ontologies. In: Fontaine, P., Schmidt, R., Schulz, S. (eds.) PAAR-2012: IJCAR\u201912 Workshop on Practical Aspects of Automated Reasoning, pp. 163\u2013177 (2012)","DOI":"10.29007\/n1sv"}],"container-title":["Mathematics in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11786-012-0135-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11786-012-0135-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11786-012-0135-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,23]],"date-time":"2025-04-23T20:43:40Z","timestamp":1745441020000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11786-012-0135-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,12]]},"references-count":29,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2012,12]]}},"alternative-id":["135"],"URL":"https:\/\/doi.org\/10.1007\/s11786-012-0135-4","relation":{},"ISSN":["1661-8270","1661-8289"],"issn-type":[{"type":"print","value":"1661-8270"},{"type":"electronic","value":"1661-8289"}],"subject":[],"published":{"date-parts":[[2012,12]]}}}