{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:58:38Z","timestamp":1725494318395},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540662228"},{"type":"electronic","value":"9783540486602"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48660-7_7","type":"book-chapter","created":{"date-parts":[[2007,11,9]],"date-time":"2007-11-09T20:53:07Z","timestamp":1194641587000},"page":"97-111","source":"Crossref","is-referenced-by-count":3,"title":["Solving Equational Problems Efficiently"],"prefix":"10.1007","author":[{"given":"Reinhard","family":"Pichler","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,5,17]]},"reference":[{"unstructured":"F. Baader, J.H. Siekmann: Unification Theory, in Handbook of Logic in Artificial Intelligence and Logic Programming, D.M. Gabbay, C.J. Hogger, J.A. Robinson (eds.), Oxford University Press (1994).","key":"7_CR1"},{"key":"7_CR2","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1006\/inco.1994.1056","volume":"112","author":"H. Comon","year":"1994","unstructured":"H. Comon, C. Delor: Equational Formulae with Membership Constraints, Journal of Information and Computation, Vol 112, pp. 167\u2013216 (1994).","journal-title":"Journal of Information and Computation"},{"key":"7_CR3","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1016\/S0747-7171(89)80017-3","volume":"7","author":"H. Comon","year":"1989","unstructured":"H. Comon, P. Lescanne: Equational Problems and Disunification, Journal of Symbolic Computation, Vol 7, pp. 371\u2013425 (1989).","journal-title":"Equational Problems and Disunification, Journal of Symbolic Computation"},{"unstructured":"R. Caferra, N. Peltier: Extending semantic Resolution via automated Model Building: applications, Proceedings of IJCAI\u201995, Morgan Kaufmann, (1995)","key":"7_CR4"},{"unstructured":"R. Caferra, N. Zabel: Extending Resolution for Model Construction, in Proceedings of Logics in AI-JELIA\u201990, LNAI 478, pp. 153\u2013169, Springer (1991).","key":"7_CR5"},{"issue":"2","key":"7_CR6","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1093\/logcom\/6.2.173","volume":"6","author":"C. Ferm\u00fcller","year":"1996","unstructured":"C. Ferm\u00fcller, A. Leitsch: Hyperresolution and Automated Model Building, Journal of Logic and Computation, Vol 6 No 2, pp.173\u2013230 (1996).","journal-title":"Journal of Logic and Computation"},{"unstructured":"G. Gottlob, R. Pichler: Working with ARMs: Complexity Results on Atomic Representations of Herbrand Models, to appear in Proceedings of LICS\u201999, IEEE Computer Society Press, (1999).","key":"7_CR7"},{"key":"7_CR8","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1007\/BF00243794","volume":"3","author":"J.-L. Lassez","year":"1987","unstructured":"J.-L. Lassez, K. Marriott: Explicit Representation of Terms defined by Counter Examples, Journal of Automated Reasoning, Vol 3, pp. 301\u2013317 (1987).","journal-title":"Journal of Automated Reasoning"},{"key":"7_CR9","series-title":"Lect Notes Comput Sci","first-page":"1","volume-title":"Proceedings of MFCS\u201991","author":"J.-L. Lassez","year":"1991","unstructured":"J.-L. Lassez, M. Maher, K. Marriott: Elimination of Negation in Term Algebras, in Proceedings of MFCS\u201991, LNCS 520, pp. 1\u201316, Springer (1991)."},{"unstructured":"D. Lugiez: A Deduction Procedure for First Order Programs, in Proceedings of ICLP\u201989, pp. 585\u2013599, Lisbon (1989).","key":"7_CR10"},{"doi-asserted-by":"crossref","unstructured":"M. Maher: Complete Axiomatizations of the Algebras of Finite, Rational and Infinite Trees, in Proceedings of LICS\u201988, pp. 348\u2013357, IEEE Computer Society Press, (1988).","key":"7_CR11","DOI":"10.1109\/LICS.1988.5132"},{"issue":"2","key":"7_CR12","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1145\/357162.357169","volume":"4","author":"A. Martelli","year":"1982","unstructured":"A. Martelli, U. Montanari: An efficient unification algorithm, ACM Transactions on Programming Languages and Systems, Vol 4 No 2, pp. 258\u2013282 (1982).","journal-title":"ACM Transactions on Programming Languages and Systems"},{"unstructured":"R. Pichler: Algorithms on Atomic Representations of Herbrand Models, in Proceedings of Logics in AI-JELIA\u201998, LNAI 1489, pp. 199\u2013215, Springer (1998).","key":"7_CR13"},{"issue":"1","key":"7_CR14","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J.A. Robinson","year":"1965","unstructured":"J.A. Robinson: A machine oriented logic based on the resolution principle, Journal of the ACM, Vol 12, No 1, pp. 23\u201341 (1965).","journal-title":"Journal of the ACM"},{"unstructured":"T. Sato, F. Motoyoshi: A complete Top-down Interpreter for First Order Programs, in Proceedings of ILPS\u201991, pp. 35\u201353, (1991).","key":"7_CR15"},{"unstructured":"S. Vorobyov: An Improved Lower Bound for the Elementary Theories of Trees, in Proceedings of CADE-13, LNAI 1104, pp. 275\u2013287, Springer (1996).","key":"7_CR16"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2014 CADE-16"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48660-7_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,25]],"date-time":"2019-02-25T02:43:44Z","timestamp":1551062624000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48660-7_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540662228","9783540486602"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/3-540-48660-7_7","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}