{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T21:10:34Z","timestamp":1725570634968},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642175107"},{"type":"electronic","value":"9783642175114"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-17511-4_17","type":"book-chapter","created":{"date-parts":[[2010,12,7]],"date-time":"2010-12-07T06:24:40Z","timestamp":1291703080000},"page":"290-311","source":"Crossref","is-referenced-by-count":2,"title":["Disunification for Ultimately Periodic Interpretations"],"prefix":"10.1007","author":[{"given":"Matthias","family":"Horbach","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"17_CR1","doi-asserted-by":"crossref","unstructured":"Baader, F., Snyder, W.: Unification theory. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol.\u00a01, ch.\u00a08, pp. 445\u2013532. Elsevier and MIT Press (2001)","DOI":"10.1016\/B978-044450813-3\/50010-2"},{"key":"17_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1007\/3-540-59200-8_60","volume-title":"Rewriting Techniques and Applications","author":"L. Bachmair","year":"1995","unstructured":"Bachmair, L., Plaisted, D.A.: Associative path orderings. In: Hsiang, J. (ed.) RTA 1995. LNCS, vol.\u00a0914, pp. 241\u2013254. Springer, Heidelberg (1995)"},{"issue":"6","key":"17_CR3","doi-asserted-by":"publisher","first-page":"613","DOI":"10.1016\/S0747-7171(10)80014-8","volume":"13","author":"R. Caferra","year":"1992","unstructured":"Caferra, R., Zabel, N.: A method for simultaneous search for refutations and models by equational constraint solving. Journal of Symbolic Computation\u00a013(6), 613\u2013642 (1992)","journal-title":"Journal of Symbolic Computation"},{"key":"17_CR4","first-page":"293","volume-title":"Logic and Data Bases","author":"K.L. Clark","year":"1977","unstructured":"Clark, K.L.: Negation as failure. In: Gallaire, H., Minker, J. (eds.) Logic and Data Bases, pp. 293\u2013322. Plenum Press, New York (1977)"},{"key":"17_CR5","unstructured":"Colmerauer, A.: Equations and inequations on finite and infinite trees. In: FGCS, vol.\u00a05, pp. 85\u201399 (1984)"},{"key":"17_CR6","unstructured":"Comon, H.: Unification et Disunification: Th\u00e9orie et applications. PhD thesis, Institut National Polytechnique de Grenoble (July 1988)"},{"key":"17_CR7","first-page":"322","volume-title":"Computational Logic: Essays in Honor of Alan Robinson","author":"H. Comon","year":"1991","unstructured":"Comon, H.: Disunification: A survey. In: Lassez, J.-L., Plotkin, G. (eds.) Computational Logic: Essays in Honor of Alan Robinson, pp. 322\u2013359. MIT Press, Cambridge (1991)"},{"issue":"2","key":"17_CR8","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1006\/inco.1994.1056","volume":"112","author":"H. Comon","year":"1994","unstructured":"Comon, H., Delor, C.: Equational formulae with membership constraints. Information and Computation\u00a0112(2), 167\u2013216 (1994)","journal-title":"Information and Computation"},{"issue":"3-4","key":"17_CR9","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1016\/S0747-7171(89)80017-3","volume":"7","author":"H. Comon","year":"1989","unstructured":"Comon, H., Lescanne, P.: Equational problems and disunification. Journal of Symbolic Computation\u00a07(3-4), 371\u2013425 (1989)","journal-title":"Journal of Symbolic Computation"},{"issue":"1\/2","key":"17_CR10","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1006\/inco.2000.2875","volume":"159","author":"H. Comon","year":"2000","unstructured":"Comon, H., Nieuwenhuis, R.: Induction = I-axiomatization + first-order consistency. Information and Computation\u00a0159(1\/2), 151\u2013186 (2000)","journal-title":"Information and Computation"},{"key":"17_CR11","doi-asserted-by":"publisher","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. Theoretical Computer Science\u00a017, 279\u2013301 (1982)","journal-title":"Theoretical Computer Science"},{"issue":"2","key":"17_CR12","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1093\/logcom\/6.2.173","volume":"6","author":"C.G. Ferm\u00fcller","year":"1996","unstructured":"Ferm\u00fcller, C.G., Leitsch, A.: Hyperresolution and automated model building. Journal of Logic and Computation\u00a06(2), 173\u2013203 (1996)","journal-title":"Journal of Logic and Computation"},{"key":"17_CR13","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BF01189020","volume":"3","author":"M. Fern\u00e1ndez","year":"1992","unstructured":"Fern\u00e1ndez, M.: Narrowing based procedures for equational disunification. Applicable Algebra in Engineering, Communication and Computing\u00a03, 1\u201326 (1992)","journal-title":"Applicable Algebra in Engineering, Communication and Computing"},{"key":"17_CR14","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"404","DOI":"10.1007\/978-3-642-02959-2_30","volume-title":"Automated Deduction \u2013 CADE-22","author":"M. Horbach","year":"2009","unstructured":"Horbach, M., Weidenbach, C.: Decidability results for saturation-based model building. In: Schmidt, R.A. (ed.) CADE 2009. LNCS (LNAI), vol.\u00a05663, pp. 404\u2013420. Springer, Heidelberg (2009)"},{"key":"17_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"332","DOI":"10.1007\/978-3-642-04027-6_25","volume-title":"Computer Science Logic","author":"M. Horbach","year":"2009","unstructured":"Horbach, M., Weidenbach, C.: Deciding the inductive validity of \u2200\u2009\u2203\u2009* queries. In: Gr\u00e4del, E., Kahle, R. (eds.) CSL 2009. LNCS, vol.\u00a05771, pp. 332\u2013347. Springer, Heidelberg (2009)"},{"key":"17_CR16","first-page":"257","volume-title":"Computational Logic - Essays in Honor of Alan Robinson","author":"J.-P. Jouannaud","year":"1991","unstructured":"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\u2013321. MIT Press, Cambridge (1991)"},{"issue":"4","key":"17_CR17","doi-asserted-by":"publisher","first-page":"1155","DOI":"10.1137\/0215084","volume":"15","author":"J.-P. Jouannaud","year":"1986","unstructured":"Jouannaud, J.-P., Kirchner, H.: Completion of a set of rules modulo a set of equations. SIAM J. Comput.\u00a015(4), 1155\u20131194 (1986)","journal-title":"SIAM J. Comput."},{"key":"17_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/3-540-19129-1_4","volume-title":"Foundations of Logic and Functional Programming","author":"J.-L. Lassez","year":"1988","unstructured":"Lassez, J.-L., Maher, M.J., Marriott, K.: Unification revisited. In: Boscarol, M., Levi, G., Aiello, L.C. (eds.) Foundations of Logic and Functional Programming. LNCS, vol.\u00a0306, pp. 67\u2013113. Springer, Heidelberg (1988)"},{"key":"17_CR19","first-page":"73","volume-title":"TIME","author":"M. Ludwig","year":"2009","unstructured":"Ludwig, M., Hustadt, U.: Resolution-based model construction for PLTL. In: Lutz, C., Raskin, J.-F. (eds.) TIME, pp. 73\u201380. IEEE Computer Society, Los Alamitos (2009)"},{"key":"17_CR20","first-page":"348","volume-title":"LICS","author":"M.J. Maher","year":"1988","unstructured":"Maher, M.J.: Complete axiomatizations of the algebras of finite, rational and infinite trees. In: LICS, pp. 348\u2013357. IEEE Computer Society, Los Alamitos (1988)"},{"key":"17_CR21","first-page":"262","volume-title":"The Metamathematics of Algebraic Systems: Collected Papers 1936\u20131967","author":"A.I. Mal\u2019cev","year":"1971","unstructured":"Mal\u2019cev, A.I.: Axiomatizable classes of locally free algebra of various type. In: Wells, B.F. (ed.) The Metamathematics of Algebraic Systems: Collected Papers 1936\u20131967,\u00a0ch.\u00a023, pp. 262\u2013281. North Holland, Amsterdam (1971)"},{"key":"17_CR22","unstructured":"Plotkin, G.: Building in equational theories. In: Meltzer, B.N., Michie, D. (eds.) Machine Intelligence, vol.\u00a07, pp. 73\u201390. Edinburgh University Press (1972)"},{"issue":"1","key":"17_CR23","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J.A. Robinson","year":"1965","unstructured":"Robinson, J.A.: A machine-oriented logic based on the resolution principle. Journal of the ACM\u00a012(1), 23\u201341 (1965)","journal-title":"Journal of the ACM"},{"issue":"4","key":"17_CR24","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/s10817-009-9143-8","volume":"43","author":"G. Sutcliffe","year":"2009","unstructured":"Sutcliffe, G.: The TPTP problem library and associated infrastructure. Journal of Automomated Reasoning\u00a043(4), 337\u2013362 (2009)","journal-title":"Journal of Automomated Reasoning"},{"key":"17_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1007\/978-3-642-02959-2_10","volume-title":"Automated Deduction \u2013 CADE-22","author":"C. Weidenbach","year":"2009","unstructured":"Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: SPASS version 3.5. In: Schmidt, R.A. (ed.) Automated Deduction \u2013 CADE-22. LNCS, vol.\u00a05663, pp. 140\u2013145. Springer, Heidelberg (2009)"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-17511-4_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,22]],"date-time":"2019-03-22T17:38:53Z","timestamp":1553276333000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-17511-4_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642175107","9783642175114"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-17511-4_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}