{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T12:05:54Z","timestamp":1749125154615},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540536864"},{"type":"electronic","value":"9783540469827"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1991]]},"DOI":"10.1007\/bfb0018439","type":"book-chapter","created":{"date-parts":[[2005,11,22]],"date-time":"2005-11-22T00:30:30Z","timestamp":1132619430000},"page":"153-169","source":"Crossref","is-referenced-by-count":16,"title":["Extending resolution for model construction"],"prefix":"10.1007","author":[{"given":"Ricardo","family":"Caferra","sequence":"first","affiliation":[]},{"given":"Nicolas","family":"Zabel","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,9]]},"reference":[{"key":"10_CR1","unstructured":"W. Ackermann. Solvable cases for the decision problem. North-Holland, 1954."},{"key":"10_CR2","doi-asserted-by":"crossref","unstructured":"W. W. Bledsoe and D. W. Loveland, editors. Automated theorem proving after 25 years, volume 29. Contemporary Mathematics, 1984.","DOI":"10.1090\/conm\/029"},{"key":"10_CR3","doi-asserted-by":"crossref","unstructured":"T. Boy de la Tour, R. Caferra, and G. Chaminade. Some tools for an inference laboratory (atinf). In Proc. of CADE 9, pages 744\u2013745. Springer-Verlag LNCS 310, 1988.","DOI":"10.1007\/BFb0012877"},{"key":"10_CR4","doi-asserted-by":"crossref","unstructured":"H. B\u00fcrckert. Solving disequations in equational theories. In Proc. of CADE 9, pages 517\u2013526. Springer-Verlag LNCS 310, 1988.","DOI":"10.1007\/BFb0012853"},{"key":"10_CR5","unstructured":"R. Caferra and N. Zabel. Une extension des tableaux s\u00e9mantiques utilisant les probl\u00e8mes \u00e9quationnels pour guider la recherche de mod\u00e8les et de r\u00e9futations. In Actes 3\u00e8me Journ\u00e9es Nationales PRC-GRD Intelligence Artificielle, pages 213\u2013222. \u00c9d. H\u00e8rmes, 1990."},{"key":"10_CR6","unstructured":"H. Comon. Disunification: a survey. Technical Report 540, L.R.I, Universit\u00e9 Paris-Sud, 1990. to appear in \u201cFestschrift for Robinson\u201d (J.L. Lassez and G.Plotkin, eds.) MIT Press 1990."},{"key":"10_CR7","first-page":"371","volume":"7","author":"H. Comon","year":"1989","unstructured":"H. Comon and P. Lescanne. Equational problem and disunification. JSC, 7:371\u2013425, 1989.","journal-title":"JSC"},{"issue":"2","key":"10_CR8","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1145\/5383.5389","volume":"33","author":"V. J. Digricoli","year":"1986","unstructured":"V. J. Digricoli and M. C. Harrison. Equality based binary resolution. JACM, 33(2):253\u2013289, 1986.","journal-title":"JACM"},{"key":"10_CR9","unstructured":"B. Dreben and W. D. Goldfarb. The decision problem \u2014 Solvable Classes of Quantificational Formulas. Addison-Wesley, 1979."},{"key":"10_CR10","unstructured":"J. H. Gallier. Logic for Computer Science. Harper & Row, 1986."},{"key":"10_CR11","doi-asserted-by":"crossref","unstructured":"J. Jaffar and J.-L. Lassez. Constraint logic programming. In Proc. of 14 th ACM Symp. on Princ. of Prog. Lang., pages 111\u2013119, Munich, 1987.","DOI":"10.1145\/41625.41635"},{"issue":"3","key":"10_CR12","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1145\/321958.321960","volume":"23","author":"W. H. Joyner","year":"1976","unstructured":"W. H. Joyner. Resolution strategies as decision procedures. JACM, 23(3):253\u2013417, 1976.","journal-title":"JACM"},{"key":"10_CR13","doi-asserted-by":"crossref","unstructured":"C. Kirchner and H. Kirchner. Constrained equational reasoning. In Proc of the ACM SIGSAM \u2014 Int. Symp. Symbolic and Algebraic Computation, pages 382\u2013389, Portland, U.S.A, 1989.","DOI":"10.1145\/74540.74585"},{"key":"10_CR14","unstructured":"C. Kirchner and P. Lescanne. Solving disequations. Technical Report 686, INRIA, 1987."},{"key":"10_CR15","unstructured":"D. W. Loveland. Automatic Theorem Proving: a logical basis. North Holland, 1978."},{"key":"10_CR16","unstructured":"M. Rusinowitch. D\u00e9monstration automatique par des techniques de r\u00e9\u00e9criture. Inter Editions, Paris, 1989."},{"issue":"4","key":"10_CR17","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1007\/BF00244275","volume":"1","author":"M. E. Stickel","year":"1985","unstructured":"M. E. Stickel. Automated deduction by theory resolution. JAR, 1(4):333\u2013355, 1985.","journal-title":"JAR"},{"issue":"2","key":"10_CR18","doi-asserted-by":"crossref","first-page":"273","DOI":"10.1145\/322307.322308","volume":"29","author":"S. Winker","year":"1982","unstructured":"S. Winker. Generation and verification of finite models and counter-examples using an automated theorem prover answering two open questions. JACM, 29(2):273\u2013284, 1982.","journal-title":"JACM"},{"key":"10_CR19","unstructured":"L. Wos. Automated reasoning: 33 basic research problems. Prentice-Hall, 1988."},{"key":"10_CR20","doi-asserted-by":"crossref","unstructured":"L. Wos and S. Winker. Open questions solved with the assistance of AURA, 1984. in [2].","DOI":"10.1090\/conm\/029\/05"},{"key":"10_CR21","first-page":"1","volume":"121","author":"N. Zamov","year":"1972","unstructured":"N. Zamov. On a bound for a complexity of terms in the resolution method. In Proc. Steklov of Inst. Math. 121, pages 1\u201310, 1972.","journal-title":"Proc. Steklov of Inst. Math."}],"container-title":["Lecture Notes in Computer Science","Logics in AI"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0018439","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,10]],"date-time":"2020-04-10T22:36:37Z","timestamp":1586558197000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0018439"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1991]]},"ISBN":["9783540536864","9783540469827"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/bfb0018439","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1991]]}}}