{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:48:11Z","timestamp":1749124091310},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540593386"},{"type":"electronic","value":"9783540492351"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/3-540-59338-1_35","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T12:13:40Z","timestamp":1330258420000},"page":"169-184","source":"Crossref","is-referenced-by-count":2,"title":["Link deletion in model elimination"],"prefix":"10.1007","author":[{"given":"Klaus","family":"Mayr","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"unstructured":"P. Baumgartner. Linear Completion: Combining the Linear and Unit-Resulting Restrictions. Research Report 9\/93, University of Koblenz, 1993.","key":"12_CR1"},{"unstructured":"P. Baumgartner. Refinements of Theory Model Elimination and a Variant without Contrapositives. Proceedings of the 11th. European Conference on Artificial Intelligence, ECAI'94. pages 90\u201394, 1994.","key":"12_CR2"},{"doi-asserted-by":"crossref","unstructured":"P. Baumgartner and U. Furbach. Model Elimination without Contrapositives and its Application to PTTP. 12th. Conference on Automated Reasoning, CADE'94, Lecture Notes in Artificial Intelligence 814, pages 87\u2013101. Springer, 1994.","key":"12_CR3","DOI":"10.1007\/3-540-58156-1_7"},{"unstructured":"N. Eisinger. Completeness, confluence, and related properties of clause graph resolution. Dissertation, SEKI Report SR-88-07, Informatik, Universit\u00e4t Kaiserslautern. 1988.","key":"12_CR4"},{"key":"12_CR5","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1016\/0004-3702(91)90098-5","volume":"50","author":"N. Eisinger","year":"1991","unstructured":"N. Eisinger and H. J. Ohlbach and A. Pr\u00e4cklein. Reduction rules for resolution-based systems Artificial Intelligence, 50, 141\u2013181, 1991.","journal-title":"Artificial Intelligence"},{"key":"12_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":"R. A. Kowalski and D. Kuehner. Linear Resolution with Selection Function. Artificial Intelligence, 2:227\u2013260, 1971.","journal-title":"Artificial Intelligence"},{"key":"12_CR7","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1007\/BF00244282","volume":"8","author":"R. Letz","year":"1992","unstructured":"R. Letz, J. Schumann, S. Bayerl, and W. Bibel. SETHEO: A High-Performance Theorem Prover. Journal of Automated Reasoning, 8:183\u2013212, 1992.","journal-title":"Journal of Automated Reasoning"},{"key":"12_CR8","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1007\/BF00881947","volume":"13","author":"R. Letz","year":"1994","unstructured":"R. Letz, K. Mayr, and C. Goller. Controlled Integrations of the Cut Rule into Connection Ta bleau Calculi. Journal of Automated Reasonig, 13: 297\u2013337, 1994.","journal-title":"Journal of Automated Reasonig"},{"issue":"2","key":"12_CR9","doi-asserted-by":"crossref","first-page":"236","DOI":"10.1145\/321450.321456","volume":"15","author":"D. W. Loveland","year":"1968","unstructured":"D. W. Loveland. Mechanical Theorem Proving by Model Elimination. Journal of the Association for Computing Machinery, 15(2):236\u2013251, 1968.","journal-title":"Journal of the Association for Computing Machinery"},{"unstructured":"D. W. Loveland. Automated Theorem Proving: a Logical Basis. North-Holland, 1978.","key":"12_CR10"},{"doi-asserted-by":"crossref","unstructured":"K. Mayr. Refinements and Extensions of Model Elimination. 4th. Conference on Logic Programming and Automated Reasoning, LPAR'93. Lecture Notes in Artificial Intelligence 698, pages 217\u2013228. Springer, 1993.","key":"12_CR11","DOI":"10.1007\/3-540-56944-8_55"},{"unstructured":"K. Mayr. Verfeinerungen und Erweiterungen der Modellelimination. Dissertation, Technische Unversit\u00e4t M\u00fcnchen. To appear in 1995.","key":"12_CR12"},{"issue":"4","key":"12_CR13","first-page":"389","volume":"6","author":"D. Plaisted","year":"1990","unstructured":"D. Plaisted. A Sequent-Style Model Elimination Strategy and a Positive Refinement. Journal of Automated Reasoing, 6(4):389\u2013402, 1990.","journal-title":"Journal of Automated Reasoing"},{"doi-asserted-by":"crossref","unstructured":"C.B. Suttner, G. Sutcliffe, and T. Yemenis. The TPTP Problem Library (TPTP v1.0.0 \u2014 TR Date 8.12.93). 12th. Conference on Automated Reasoning, CADE'94, Lecture Notes in Artificial Intelligence 814, pages 252\u2013266. Springer, 1994.","key":"12_CR14","DOI":"10.1007\/3-540-58156-1_18"}],"container-title":["Lecture Notes in Computer Science","Theorem Proving with Analytic Tableaux and Related Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-59338-1_35.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T16:26:51Z","timestamp":1605630411000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-59338-1_35"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540593386","9783540492351"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/3-540-59338-1_35","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]}}}