{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:29:25Z","timestamp":1750307365934,"version":"3.41.0"},"reference-count":28,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2010,7,1]],"date-time":"2010-07-01T00:00:00Z","timestamp":1277942400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["SFB\/TR 14 AVACS"],"award-info":[{"award-number":["SFB\/TR 14 AVACS"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2010,7]]},"abstract":"<jats:p>Superposition is an established decision procedure for a variety of first-order logic theories represented by sets of clauses. A satisfiable theory, saturated by superposition, implicitly defines a minimal term-generated model for the theory. Proving universal properties with respect to a saturated theory directly leads to a modification of the minimal model's term-generated domain, as new Skolem functions are introduced. For many applications, this is not desired.<\/jats:p>\n          <jats:p>Therefore, we propose the first superposition calculus that can explicitly represent existentially quantified variables and can thus compute with respect to a given domain. This calculus is sound and refutationally complete in the limit for a first-order fixed domain semantics. For saturated Horn theories and classes of positive formulas, we can even employ the calculus to prove properties of the minimal model itself, going beyond the scope of known superposition-based approaches.<\/jats:p>","DOI":"10.1145\/1805950.1805957","type":"journal-article","created":{"date-parts":[[2010,7,15]],"date-time":"2010-07-15T12:48:46Z","timestamp":1279198126000},"page":"1-35","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["Superposition for fixed domains"],"prefix":"10.1145","volume":"11","author":[{"given":"Matthias","family":"Horbach","sequence":"first","affiliation":[{"name":"Max Planck Institute for Informatics, Saarbr\u00fccken, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christoph","family":"Weidenbach","sequence":"additional","affiliation":[{"name":"Max Planck Institute for Informatics, Saarbr\u00fccken, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2010,7,20]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/1459010.1459014"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/4.3.217"},{"key":"e_1_2_1_3_1","volume-title":"Proceedings of the 3rd Kurt G\u00f6del Colloquium on Computational Logic and Proof Theory (KGC'93)","volume":"713","author":"Bachmair L.","unstructured":"Bachmair , L. , Ganzinger , H. , and Waldmann , U . 1993. Superposition with simplification as a decision procedure for the monadic class with equality . In Proceedings of the 3rd Kurt G\u00f6del Colloquium on Computational Logic and Proof Theory (KGC'93) . Lecture Notes in Computer Science , vol. 713 . Springer-Verlag, Berlin, 83--96. Bachmair, L., Ganzinger, H., and Waldmann, U. 1993. Superposition with simplification as a decision procedure for the monadic class with equality. In Proceedings of the 3rd Kurt G\u00f6del Colloquium on Computational Logic and Proof Theory (KGC'93). Lecture Notes in Computer Science, vol. 713. Springer-Verlag, Berlin, 83--96."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1006\/jsco.1996.0076"},{"volume-title":"Proceedings of the 12th IEEE Symposium on Logic in Computer Science. IEEE, 14","author":"Bouhoula A.","key":"e_1_2_1_5_1","unstructured":"Bouhoula , A. and Jouannaud , J . -P. 1997. Automata-driven automated induction . In Proceedings of the 12th IEEE Symposium on Logic in Computer Science. IEEE, 14 . Bouhoula, A. and Jouannaud, J.-P. 1997. Automata-driven automated induction. In Proceedings of the 12th IEEE Symposium on Logic in Computer Science. IEEE, 14."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(10)80014-8"},{"key":"e_1_2_1_7_1","volume-title":"Disunification: A survey. In Computational Logic: Essays in Honor of Alan Robinson, J.-L","author":"Comon H.","year":"1991","unstructured":"Comon , H. 1991 . Disunification: A survey. In Computational Logic: Essays in Honor of Alan Robinson, J.-L . Lassez and G. Plotkin, Eds. MIT Press, Cambridge , MA , 322--359. Comon, H. 1991. Disunification: A survey. In Computational Logic: Essays in Honor of Alan Robinson, J.-L. Lassez and G. Plotkin, Eds. MIT Press, Cambridge, MA, 322--359."},{"volume-title":"Proceedings of the 12th Annual IEEE Symposium on Logic in Computer Science (LICS'97)","author":"Comon H.","key":"e_1_2_1_8_1","unstructured":"Comon , H. and Jacquemard , F . 1997. Ground reducability is exptime-complete . In Proceedings of the 12th Annual IEEE Symposium on Logic in Computer Science (LICS'97) . IEEE Computer Society Press, Los Alamitos, CA, 26--34. Comon, H. and Jacquemard, F. 1997. Ground reducability is exptime-complete. In Proceedings of the 12th Annual IEEE Symposium on Logic in Computer Science (LICS'97). IEEE Computer Society Press, Los Alamitos, CA, 26--34."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(89)80017-3"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2000.2875"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/11916277_4"},{"volume-title":"Proceedings of the 14th IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press","author":"Ganzinger H.","key":"e_1_2_1_12_1","unstructured":"Ganzinger , H. and Nivelle , H. D . 1999. A superposition decision procedure for the guarded fragment with equality . In Proceedings of the 14th IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press , Los Alamitos, CA, 295--305. Ganzinger, H. and Nivelle, H. D. 1999. A superposition decision procedure for the guarded fragment with equality. In Proceedings of the 14th IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, Los Alamitos, CA, 295--305."},{"key":"e_1_2_1_13_1","volume-title":"Lecture Notes in Computer Science","volume":"656","author":"Ganzinger H.","unstructured":"Ganzinger , H. and Stuber , J . 1992. Inductive theorem proving by consistency for first-order clauses. In Informatik - Festschrift zum 60. Geburtstag von G\u00fcnter Hotz, J. Buchmann, H. Ganzinger, and W. Paul, Eds. Teubner, 441--462 . Lecture Notes in Computer Science , vol. 656 , Springer-Verlag, Berlin. Ganzinger, H. and Stuber, J. 1992. Inductive theorem proving by consistency for first-order clauses. In Informatik - Festschrift zum 60. Geburtstag von G\u00fcnter Hotz, J. Buchmann, H. Ganzinger, and W. Paul, Eds. Teubner, 441--462. Lecture Notes in Computer Science, vol. 656, Springer-Verlag, Berlin."},{"key":"e_1_2_1_14_1","volume-title":"Proceedings of the 19th International Conference on Automated Deduction (CADE'19)","volume":"2741","author":"Giesl J.","unstructured":"Giesl , J. and Kapur , D . 2003. Deciding inductive validity of equations . In Proceedings of the 19th International Conference on Automated Deduction (CADE'19) . Lecture Notes in Computer Science , vol. 2741 . Springer, Berlin, 17--31. Giesl, J. and Kapur, D. 2003. Deciding inductive validity of equations. In Proceedings of the 19th International Conference on Automated Deduction (CADE'19). Lecture Notes in Computer Science, vol. 2741. Springer, Berlin, 17--31."},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02959-2_30"},{"key":"e_1_2_1_16_1","doi-asserted-by":"crossref","unstructured":"Horbach M.\n     and \n      Weidenbach C\n  . \n  2009\n  b. Deciding the inductive validity of &forall;&exists;&ast; queries. In Proceedings of the 18th Annual Conference of the European Association for Computer Science Logic (CSL'09) Lecture Notes in Computer Science vol. \n  5771\n  . \n  Springer-Verlag Berlin 332--347.   Horbach M. and Weidenbach C. 2009b. Deciding the inductive validity of &forall;&exists; &ast; queries. In Proceedings of the 18th Annual Conference of the European Association for Computer Science Logic (CSL'09) Lecture Notes in Computer Science vol. 5771. Springer-Verlag Berlin 332--347.","DOI":"10.1007\/978-3-642-04027-6_25"},{"key":"e_1_2_1_17_1","first-page":"251","article-title":"A survey of decidable first-order fragments and description logics","volume":"1","author":"Hustadt U.","year":"2004","unstructured":"Hustadt , U. , Schmidt , R. A. , and Georgieva , L. 2004 . A survey of decidable first-order fragments and description logics . J. Relat. Meth. Comput. Sci. 1 , 251 -- 276 . Hustadt, U., Schmidt, R. A., and Georgieva, L. 2004. A survey of decidable first-order fragments and description logics. J. Relat. Meth. Comput. Sci. 1, 251--276.","journal-title":"J. Relat. Meth. Comput. Sci."},{"key":"e_1_2_1_18_1","volume-title":"Proceedings of the 9th International Conference on Rewriting Techniques and Applications (RTA'98)","volume":"1379","author":"Jacquemard F.","unstructured":"Jacquemard , F. , Meyer , C. , and Weidenbach , C . 1998. Unification in extensions of shallow equational theories . In Proceedings of the 9th International Conference on Rewriting Techniques and Applications (RTA'98) . Lecture Notes in Computer Science , vol. 1379 . Springer-Verlag, Berlin, 76--90. Jacquemard, F., Meyer, C., and Weidenbach, C. 1998. Unification in extensions of shallow equational theories. In Proceedings of the 9th International Conference on Rewriting Techniques and Applications (RTA'98). Lecture Notes in Computer Science, vol. 1379. Springer-Verlag, Berlin, 76--90."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/11814771_45"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(08)80133-2"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/648236.753792"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90279-O"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/788018.788824"},{"key":"e_1_2_1_24_1","first-page":"371","article-title":"Paramodulation-based theorem proving. In Handbook of Automated Reasoning, A. Robinson and A. Voronkov, Eds. Vol. I. Elsevier, Amsterdam, The Netherlands","volume":"7","author":"Nieuwenhuis R.","year":"2001","unstructured":"Nieuwenhuis , R. and Rubio , A. 2001 . Paramodulation-based theorem proving. In Handbook of Automated Reasoning, A. Robinson and A. Voronkov, Eds. Vol. I. Elsevier, Amsterdam, The Netherlands , Chapter 7 , 371 -- 443 . Nieuwenhuis, R. and Rubio, A. 2001. Paramodulation-based theorem proving. In Handbook of Automated Reasoning, A. Robinson and A. Voronkov, Eds. Vol. I. Elsevier, Amsterdam, The Netherlands, Chapter 7, 371--443.","journal-title":"Chapter"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(03)00028-2"},{"key":"e_1_2_1_26_1","doi-asserted-by":"crossref","unstructured":"Plaisted D. A. 1985. Semantic confluence tests and completion methods. Inform. Cont. 65 2\/3 182--215.  Plaisted D. A. 1985. Semantic confluence tests and completion methods. Inform. Cont. 65 2\/3 182--215.","DOI":"10.1016\/S0019-9958(85)80005-X"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.5555\/648235.753480"},{"key":"e_1_2_1_28_1","volume-title":"Handbook of Automated Reasoning","author":"Weidenbach C.","year":"1965","unstructured":"Weidenbach , C. 2001. Combining superposition, sorts and splitting . In Handbook of Automated Reasoning , A. Robinson and A. Voronkov, Eds. Vol. 2. Elsevier , Amsterdam, The Netherlands, Chapter 27, 1965 --2012. Weidenbach, C. 2001. Combining superposition, sorts and splitting. In Handbook of Automated Reasoning, A. Robinson and A. Voronkov, Eds. Vol. 2. Elsevier, Amsterdam, The Netherlands, Chapter 27, 1965--2012."}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1805950.1805957","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1805950.1805957","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T11:22:42Z","timestamp":1750245762000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1805950.1805957"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,7]]},"references-count":28,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2010,7]]}},"alternative-id":["10.1145\/1805950.1805957"],"URL":"https:\/\/doi.org\/10.1145\/1805950.1805957","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2010,7]]},"assertion":[{"value":"2008-09-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2009-10-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2010-07-20","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}