{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:23:31Z","timestamp":1725488611052},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540671909"},{"type":"electronic","value":"9783540465089"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-46508-1_14","type":"book-chapter","created":{"date-parts":[[2007,8,3]],"date-time":"2007-08-03T16:02:03Z","timestamp":1186156923000},"page":"206-220","source":"Crossref","is-referenced-by-count":0,"title":["Extending Decidable Clause Classes via Constraints"],"prefix":"10.1007","author":[{"given":"Reinhard","family":"Pichler","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,5,17]]},"reference":[{"key":"14_CR1","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":"Journal of Symbolic Computation"},{"key":"14_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"130","DOI":"10.1007\/3-540-61377-3_35","volume-title":"Proceedings of CSL\u201995","author":"R. Caferra","year":"1996","unstructured":"R. Caferra, N. Peltier: Decision Procedures using Model Building Techniques, Proceedings of CSL\u201995, LNCS 1092, pp.130\u2013144, Springer (1996)."},{"key":"14_CR3","unstructured":"R. Caferra, N. Zabel: Extending Resolution for Model Construction, Proceedings of Logics in AI-JELIA\u201990, LNAI 478, pp. 153\u2013169, Springer (1991)."},{"issue":"8","key":"14_CR4","doi-asserted-by":"publisher","first-page":"465","DOI":"10.1145\/359138.359142","volume":"22","author":"N. Dershowitz","year":"1979","unstructured":"N. Dershowitz, Z. Manna: Proving Termination with Multiset Orderings, in Communications of the ACM, Vol 22, No 8, pp. 465\u2013475 (1979).","journal-title":"Communications of the ACM"},{"key":"14_CR5","doi-asserted-by":"crossref","unstructured":"C. Ferm\u00fcller, A. Leitsch, T. Tammet, N. Zamov: Resolution Methods for the Decision Problem. LNAI 679, Springer (1993).","DOI":"10.1007\/3-540-56732-1"},{"key":"14_CR6","first-page":"87","volume":"4","author":"R. Kowalski","year":"1969","unstructured":"R. Kowalski, P.J. Hayes: Semantic Trees in Automated Theorem Proving, in Machine Intelligence 4, pp. 87\u2013101 (1969).","journal-title":"Machine Intelligence"},{"key":"14_CR7","unstructured":"A. Leitsch: The Resolution Calculus, Texts in Theoretical Computer Science, Springer (1997)."},{"key":"14_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":"14_CR9","series-title":"Lect Notes Comput Sci","first-page":"67","volume-title":"Unification Revisited, Foundations of Logic and Functional Programming","author":"J.-L. Lassez","year":"1986","unstructured":"J.-L. Lassez, M.J. Maher, K. Marriott: Unification Revisited, Foundations of Logic and Functional Programming, LNCS 306, pp. 67\u2013113, Springer (1986)."},{"key":"14_CR10","unstructured":"R. Pichler: Completeness and Redundancy in Constrained Clause Logic, in Proceedings of FTP\u201998 (Int. Workshop on First-Order Theorem Proving), Technical Report E1852-GS-981 of Technische Universit\u00e4tWien, pp. 193\u2013203, available from \n                    http:\/\/www.logic.at\/ftp98\n                    \n                  , Vienna (1998)."},{"issue":"1","key":"14_CR11","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"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction in Classical and Non-Classical Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-46508-1_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,20]],"date-time":"2019-02-20T14:26:39Z","timestamp":1550672799000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-46508-1_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540671909","9783540465089"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/3-540-46508-1_14","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]}}}