{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T18:50:04Z","timestamp":1725475804523},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540676645"},{"type":"electronic","value":"9783540451013"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/10721959_28","type":"book-chapter","created":{"date-parts":[[2006,12,29]],"date-time":"2006-12-29T21:12:31Z","timestamp":1167426751000},"page":"365-384","source":"Crossref","is-referenced-by-count":5,"title":["Stratified Resolution"],"prefix":"10.1007","author":[{"given":"Anatoli","family":"Degtyarev","sequence":"first","affiliation":[]},{"given":"Andrei","family":"Voronkov","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"28_CR1","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1016\/B978-0-934613-40-8.50006-3","volume-title":"Foundations of Deductive Databases and Logic Programming","author":"K.R. Apt","year":"1988","unstructured":"Apt, K.R., Blair, H.A.: Towards a theory of declarative knowledge. In: Minker, J. (ed.) Foundations of Deductive Databases and Logic Programming, pp. 89\u2013148. Morgan Kaufmann, San Francisco (1988)"},{"key":"#cr-split#-28_CR2.1","unstructured":"Bachmair, L., Ganzinger, H.: A theory of resolution. Research report MPI-I-97- 2-005, Max-Planck Institut f??r Informatik, Saarbr??cken, Germany (1997);"},{"key":"#cr-split#-28_CR2.2","unstructured":"To appear in Handbook of Automated Reasoning, edited by A. Robinson and A. Voronkov"},{"key":"28_CR3","unstructured":"Bachmair, L., Ganzinger, H.: A theory of resolution. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning. Elsevier Science and MIT Press (2000)"},{"key":"28_CR4","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1006\/inco.1995.1131","volume":"121","author":"L. Bachmair","year":"1995","unstructured":"Bachmair, L., Ganzinger, H., Lynch, C., Snyder, W.: Basic paramodulation. Information and Computation\u00a0121, 172\u2013192 (1995)","journal-title":"Information and Computation"},{"key":"28_CR5","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1016\/B978-0-934613-40-8.50007-5","volume-title":"Deductive Databases and Logic Programming","author":"A. Gelder Van","year":"1988","unstructured":"Van Gelder, A.: Negation as failure using tight derivations for general logic programs. In: Minker, J. (ed.) Deductive Databases and Logic Programming, pp. 149\u2013177. Morgan Kaufmann, San Francisco (1988)"},{"key":"28_CR6","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1016\/0004-3702(71)90012-9","volume":"2","author":"R.A. Kowalski","year":"1971","unstructured":"Kowalski, R.A., Kuehner, D.: Linear resolution with selection function. Artificial Intelligence\u00a02, 227\u2013260 (1971)","journal-title":"Artificial Intelligence"},{"issue":"1","key":"28_CR7","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1006\/jsco.1996.0075","volume":"23","author":"C. Lynch","year":"1997","unstructured":"Lynch, C.: Oriented equational logic is complete. Journal of Symbolic Computations\u00a023(1), 23\u201345 (1997)","journal-title":"Journal of Symbolic Computations"},{"key":"28_CR8","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1016\/B978-0-934613-40-8.50009-9","volume-title":"Foundations of Deductive Databases and Logic Programming","author":"H. Przymusinski","year":"1988","unstructured":"Przymusinski, H.: On the declarative semantics of deductive databases and logic programs. In: Minker, J. (ed.) Foundations of Deductive Databases and Logic Programming, pp. 193\u2013216. Morgan Kaufmann, San Francisco (1988)"},{"key":"28_CR9","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1007\/3-540-48660-7_26","volume-title":"Automated Deduction - CADE-16","author":"A. Riazanov","year":"1999","unstructured":"Riazanov, A., Voronkov, A.: Vampire. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol.\u00a01632, pp. 292\u2013296. Springer, Heidelberg (1999)"},{"key":"#cr-split#-28_CR10.1","unstructured":"Voronkov, A.: How to optimize proof-search in modal logics: a new way of proving redundancy criteria for sequent calculi. Preprint 1, Department of Computer Science, University of Manchester (February 2000);"},{"key":"#cr-split#-28_CR10.2","unstructured":"To appear in LICS (2000)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction - CADE-17"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/10721959_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,23]],"date-time":"2019-03-23T10:36:32Z","timestamp":1553337392000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/10721959_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540676645","9783540451013"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/10721959_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2000]]}}}