{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:23:36Z","timestamp":1725488616799},"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_15","type":"book-chapter","created":{"date-parts":[[2007,8,3]],"date-time":"2007-08-03T16:02:03Z","timestamp":1186156923000},"page":"221-235","source":"Crossref","is-referenced-by-count":2,"title":["Completeness and Redundancy in Constrained Clause Logic"],"prefix":"10.1007","author":[{"given":"Reinhard","family":"Pichler","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,5,17]]},"reference":[{"unstructured":"Ch. Bourely, R. Caferra, N. Peltier: A Method for Building Models automatically. Experiments with an Extension of Otter. Proceedings of CADE-12, LNAI 814, pp. 72\u201386 Springer (1994).","key":"15_CR1"},{"issue":"3","key":"15_CR2","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1093\/logcom\/4.3.217","volume":"4","author":"L. Bachmair","year":"1994","unstructured":"L. Bachmair, H. Ganzinger: Rewrite-based Equational Theorem Proving with Selection and Simplification, Journal of Logic and Computation, Vol 4 No 3, pp. 217\u2013247 (1994).","journal-title":"Journal of Logic and Computation"},{"key":"15_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":"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":"15_CR4"},{"key":"15_CR5","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)."},{"unstructured":"R. Caferra, N. Zabel: Extending Resolution for Model Construction, Proceedings of Logics in AI \u2014 JELIA\u201990, LNAI 478, pp. 153\u2013169, Springer (1991).","key":"15_CR6"},{"issue":"2","key":"15_CR7","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"},{"issue":"3","key":"15_CR8","doi-asserted-by":"publisher","first-page":"559","DOI":"10.1145\/116825.116833","volume":"38","author":"J. Hsiang","year":"1991","unstructured":"J. Hsiang, M. Rusinowitch: Proving Refutational Completeness of Theorem-Proving Strategies: The Transfinite Semantic Tree Method, Journal of the ACM, Vol 38 No 3, pp. 559\u2013587 (1991).","journal-title":"Journal of the ACM"},{"key":"15_CR9","first-page":"87","volume":"4","author":"R. Kowalski","year":"1969","unstructured":"R. Kowalski, P.J. Hayes: Semantic Trees in Automated Theorem Proving, Machine Intelligence 4, pp. 87\u2013101, Edinburgh University Press (1969).","journal-title":"Semantic Trees in Automated Theorem Proving, Machine Intelligence"},{"unstructured":"A. Leitsch: The Resolution Calculus, Texts in Theoretical Computer Science, Springer (1997).","key":"15_CR10"},{"key":"15_CR11","first-page":"1","volume":"11","author":"R. Nieuwenhuis","year":"1995","unstructured":"R. Nieuwenhuis, A. Rubio: Theorem Proving with ordering and equality constrained clauses, Journal of Symbolic Computation, Vol 11, pp. 1\u201332 (1995).","journal-title":"Journal of Symbolic Computation"}],"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_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,20]],"date-time":"2019-02-20T14:25:34Z","timestamp":1550672734000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-46508-1_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540671909","9783540465089"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/3-540-46508-1_15","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]}}}