{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,13]],"date-time":"2026-03-13T22:57:11Z","timestamp":1773442631093,"version":"3.50.1"},"reference-count":73,"publisher":"Elsevier","isbn-type":[{"value":"9780444508133","type":"print"}],"license":[{"start":{"date-parts":[[2001,1,1]],"date-time":"2001-01-01T00:00:00Z","timestamp":978307200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1016\/b978-044450813-3\/50030-8","type":"book-chapter","created":{"date-parts":[[2007,6,11]],"date-time":"2007-06-11T13:04:11Z","timestamp":1181567051000},"page":"2015-2114","source":"Crossref","is-referenced-by-count":34,"title":["Model Elimination and Connection Tableau Procedures"],"prefix":"10.1016","author":[{"given":"Reinhold","family":"Letz","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gernot","family":"Stenz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/B978-044450813-3\/50030-8_bb0010","series-title":"Compilers \u2013 Principles, Techniques, and Tools","author":"Aho","year":"1986"},{"key":"10.1016\/B978-044450813-3\/50030-8_rf0015","series-title":"Principles of Compiler Design","author":"Aho","year":"1977"},{"key":"10.1016\/B978-044450813-3\/50030-8_rf0020","series-title":"Compilers \u2013 Principles, Techniques, and Tools","author":"Aho","year":"1986"},{"key":"10.1016\/B978-044450813-3\/50030-8_bb0020","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1145\/322248.322249","article-title":"Theorem proving through general matings","volume":"28","author":"Andrews","year":"1981","journal-title":"Journal of the ACM"},{"key":"10.1016\/B978-044450813-3\/50030-8_bb0025","article-title":"METEORs: High performance theorem provers using model elimination","author":"Astrachan","year":"1991","journal-title":"Technical Report DUKE-TR-1991-08, Department of Computer Science, Duke University"},{"key":"10.1016\/B978-044450813-3\/50030-8_bb0030","series-title":"Proceedings, 11th International Conference on Automated Deduction (CADE-11)","first-page":"224","article-title":"Caching and Lemmaizing in Model Elimination Theorem Provers","author":"Astrachan","year":"1992"},{"issue":"3","key":"10.1016\/B978-044450813-3\/50030-8_bb0035","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1016\/0168-0072(92)90042-X","article-title":"Complexity of resolution proofs and function introduction","volume":"57","author":"Baaz","year":"1992","journal-title":"Annals of Pure and Applied Logic"},{"key":"10.1016\/B978-044450813-3\/50030-8_bb0040","first-page":"19","article-title":"Resolution theorem proving","volume":"Vol. I","author":"Bachmair","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50030-8_bb0045","series-title":"Proceedings, 15th International Conference on Automated Deduction (CADE-15)","first-page":"175","article-title":"Elimination of Equality via Transformation with Ordering Constraints","author":"Bachmair","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50030-8_bb0050","series-title":"Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX-98)","first-page":"60","article-title":"Hyper Tableau \u2013 The Next Generation","author":"Baumgartner","year":"1998"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50030-8_bb0055","doi-asserted-by":"crossref","first-page":"205","DOI":"10.1023\/A:1005812703468","article-title":"A Disjunctive Positive Refinement of Model Elimination and its Application to Subsumption Deletion","volume":"19","author":"Baumgartner","year":"1997","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/B978-044450813-3\/50030-8_rf0065","series-title":"Proceedings of the 16th International Conference on Automated Deduction (CADE-16)","first-page":"329","article-title":"A Confluent Connection Calculus","author":"Baumgartner","year":"1999"},{"key":"10.1016\/B978-044450813-3\/50030-8_bb0065","series-title":"Proceedings of the 12th International Conference on Automated Deduction (CADE-12)","first-page":"769","article-title":"PROTEIN: A PROver with a Theory Extension INterface","author":"Baumgartner","year":"1994"},{"key":"10.1016\/B978-044450813-3\/50030-8_bb0070","article-title":"Integrating and Unifying Methods of Tableau-based Theorem Proving","author":"Beckert","year":"1998","journal-title":"PhD thesis, University of Karlsruhe, Department of Computer Science"},{"key":"10.1016\/B978-044450813-3\/50030-8_bb0075","series-title":"Proceedings, 11th International Conference on Automated Deduction (CADE-11)","first-page":"507","article-title":"An Improved Method for Adding Equality to Free Variable Semantic Tableaux","author":"Beckert","year":"1992"},{"key":"10.1016\/B978-044450813-3\/50030-8_bb0080","series-title":"Automated Deduction \u2013 A Basis for Applications","first-page":"11","article-title":"Analytic Tableaux","author":"Beckert","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50030-8_bb0085","series-title":"Proceedings of the 16th Annual International Symposium on Computer Architecture","first-page":"186","article-title":"KCM: A Knowledge Crunching Machine","author":"Benker","year":"1989"},{"key":"10.1016\/B978-044450813-3\/50030-8_bb0090","series-title":"Automated Theorem Proving","author":"Bibel","year":"1987"},{"key":"10.1016\/B978-044450813-3\/50030-8_bb0095","series-title":"Proceedings, 12th International Conference on Automated Deduction (CADE-12)","first-page":"783","article-title":"KoMeT","author":"Bibel","year":"1994"},{"key":"10.1016\/B978-044450813-3\/50030-8_bb0100","series-title":"Proceedings of the 5th International Workshop on Theorem Proving with Analytic Tableaux and Related Methods (TABLEAUX)","first-page":"110","article-title":"The disconnection method: a confluent integration of unification in the analytic framework","author":"Billon","year":"1996"},{"key":"10.1016\/B978-044450813-3\/50030-8_bb0105","series-title":"10th International Conference on Automated Deduction (CADE-10)","first-page":"558","article-title":"Minimizing the Number of Clauses by Renaming","author":"Boy de la Tour","year":"1990"},{"issue":"4","key":"10.1016\/B978-044450813-3\/50030-8_bb0110","doi-asserted-by":"crossref","first-page":"412","DOI":"10.1137\/0204036","article-title":"Proving Theorems with the Modification Method","volume":"4","author":"Brand","year":"1975","journal-title":"SIAM Journal on Computing"},{"issue":"3-4","key":"10.1016\/B978-044450813-3\/50030-8_bb0115","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1016\/S0747-7171(89)80017-3","article-title":"Equational Problems and Disunification","volume":"7","author":"Comon","year":"1989","journal-title":"Journal of Symbolic Computation"},{"key":"10.1016\/B978-044450813-3\/50030-8_bb0120","series-title":"Information Processing","first-page":"909","article-title":"A Rehabilitation of Robinson's Unification Algorithm","author":"Corbin","year":"1983"},{"key":"10.1016\/B978-044450813-3\/50030-8_bb0125","series-title":"Proceedings of the International Conference on Artificial Intelligence: Methodology, Systems and Applications (AIMSA)","first-page":"121","article-title":"An Implementation of a Theorem Prover Based on the Connection Method","author":"Eder","year":"1984"},{"key":"10.1016\/B978-044450813-3\/50030-8_bb0130","series-title":"First-Order Logic and Automated Theorem Proving","author":"Fitting","year":"1990"},{"key":"10.1016\/B978-044450813-3\/50030-8_bb0135","series-title":"First-Order Logic and Automated Theorem Proving","author":"Fitting","year":"1996"},{"key":"10.1016\/B978-044450813-3\/50030-8_rf0145","doi-asserted-by":"crossref","first-page":"176","DOI":"10.1007\/BF01201353","article-title":"Untersuchungen \u00fcber das logische Schlie\u00dfen","volume":"39","author":"Gentzen","year":"1935","journal-title":"Mathematische Zeitschrift"},{"key":"10.1016\/B978-044450813-3\/50030-8_rf0150","doi-asserted-by":"crossref","first-page":"405","DOI":"10.1007\/BF01201363","article-title":"Untersuchungen \u00fcber das logische Schlie\u00dfen","volume":"39","author":"Gentzen","year":"1935","journal-title":"Mathematische Zeitschrift"},{"key":"10.1016\/B978-044450813-3\/50030-8_bb0145","series-title":"Proceedings of the 12th International Conference on Automated Deduction (CADE-12)","first-page":"778","article-title":"SETHEO V3.2: Recent developments","author":"Goller","year":"1994"},{"key":"10.1016\/B978-044450813-3\/50030-8_bb0150","first-page":"100","article-title":"Tableaux and related methods","volume":"Vol. I","author":"H\u00e4hnle","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50030-8_rf0165","series-title":"Proceedings of the 13th International Conference on Automated Deduction (CADE-13)","first-page":"313","article-title":"Optimizing proof search in model elimination","author":"Harrison","year":"1996"},{"key":"10.1016\/B978-044450813-3\/50030-8_bb0160","series-title":"Proceedings, 12th International Conference on Automated Deduction (CADE-12)","first-page":"708","article-title":"Semantic Tableaux with Ordering Restrictions","author":"Klingenbeck","year":"1994"},{"key":"10.1016\/B978-044450813-3\/50030-8_bb0165","series-title":"Proceedings of the 9th International Joint Conference on Artificial Intelligence","first-page":"1034","article-title":"Iterative-Deepening-A: An Optimal Admissible Tree Search","author":"Korf","year":"1985"},{"key":"10.1016\/B978-044450813-3\/50030-8_bb0170","article-title":"Linear resolution with selection function","author":"Kowalski","year":"1970","journal-title":"Technical report, Metamathematics Unit, Edinburgh University, Edinburgh, Scotland"},{"key":"10.1016\/B978-044450813-3\/50030-8_bb0175","doi-asserted-by":"crossref","first-page":"227","DOI":"10.1016\/0004-3702(71)90012-9","article-title":"Linear Resolution with Selection Function","volume":"2","author":"Kowalski","year":"1971","journal-title":"Artificial Intelligence"},{"key":"10.1016\/B978-044450813-3\/50030-8_bb0180","article-title":"First-order calculi and proof procedures for automated deduction","author":"Letz","year":"1993","journal-title":"PhD thesis, Technische Hochschule Darmstadt, Darmstadt, Germany"},{"key":"10.1016\/B978-044450813-3\/50030-8_bb0185","series-title":"Automated Deduction \u2013 A Basis for Applications","first-page":"43","article-title":"Clausal Tableaux","author":"Letz","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50030-8_bb0190","series-title":"Proceedings, 15th International Conference on Automated Deduction (CADE-15)","first-page":"381","article-title":"Using Matings for Pruning Connection Tableaux","author":"Letz","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50030-8_bb0195","series-title":"Handbook of Tableau Methods","first-page":"125","article-title":"First-Order Tableaux Methods","author":"Letz","year":"1999"},{"issue":"3","key":"10.1016\/B978-044450813-3\/50030-8_bb0200","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1007\/BF00881947","article-title":"Controlled Integration of the Cut Rule into Connection Tableau Calculi","volume":"13","author":"Letz","year":"1994","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/B978-044450813-3\/50030-8_bb0205","article-title":"SETHEO: A SEquentiell THEOrem Prover for first order logic","author":"Letz","year":"1989","journal-title":"Technical Report FKI-97-89, Technische Universit\u00e4t M\u00fcnchen, Munich, Germany"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50030-8_bb0210","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1007\/BF00244282","article-title":"SETHEO: A High-Performance Theorem Prover","volume":"8","author":"Letz","year":"1992","journal-title":"Journal of Automated Reasoning"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50030-8_bb0215","doi-asserted-by":"crossref","first-page":"236","DOI":"10.1145\/321450.321456","article-title":"Mechanical Theorem Proving by Model Elimination","volume":"15","author":"Loveland","year":"1968","journal-title":"Journal of the ACM"},{"issue":"3","key":"10.1016\/B978-044450813-3\/50030-8_bb0220","doi-asserted-by":"crossref","first-page":"349","DOI":"10.1145\/321526.321527","article-title":"A Simplified Format for the Model Elimination Theorem-Proving Procedure","volume":"16","author":"Loveland","year":"1969","journal-title":"Journal of the ACM"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50030-8_bb0225","doi-asserted-by":"crossref","first-page":"366","DOI":"10.1145\/321694.321706","article-title":"A Unifying View of Some Linear Herbrand Procedures","volume":"19","author":"Loveland","year":"1972","journal-title":"Journal of the ACM"},{"key":"10.1016\/B978-044450813-3\/50030-8_bb0230","series-title":"Automated theorem proving: A logical basis","author":"Loveland","year":"1978"},{"key":"10.1016\/B978-044450813-3\/50030-8_bb0235","series-title":"Proceedings of the 4th International Conference on Logic Programming and Automated Reasoning (LPAR'93)","first-page":"217","article-title":"Refinements and Extensions of Model Elimination","author":"Mayr","year":"1993"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50030-8_bb0240","doi-asserted-by":"crossref","first-page":"237","DOI":"10.1023\/A:1005808119103","article-title":"SETHEO and E-SETHEO\u2013The CADE-13 Systems","volume":"18","author":"Moser","year":"1997","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/B978-044450813-3\/50030-8_bb0245","article-title":"Untersuchungen zum selektiven Backtracking in zielorientierten Kalk\u00fclen des automatischen Theorembeweisens","author":"Neitz","year":"1995","journal-title":"PhD thesis, University of Leipzig"},{"key":"10.1016\/B978-044450813-3\/50030-8_bb0250","series-title":"User's Guide","article-title":"ProCom\/CaPrl and the Shell ProTop","author":"Neugebauer","year":"1995"},{"key":"10.1016\/B978-044450813-3\/50030-8_bb0255","series-title":"Proceedings of the 4th International Workshop on Theorem Proving with Analytic Tableaux and Related Methods (TABLEAUX)","first-page":"185","article-title":"Specifications of Inference Rules and their Automatic Translation","author":"Neugebauer","year":"1995"},{"key":"10.1016\/B978-044450813-3\/50030-8_bb0260","first-page":"4","article-title":"Non-obviousness","author":"Pelletier","year":"1986","journal-title":"AAR Newsletter (6)"},{"key":"10.1016\/B978-044450813-3\/50030-8_bb0265","series-title":"1984 International Symposium on Logic Programming","article-title":"The Occur-check Problem in Prolog","author":"Plaisted","year":"1984"},{"issue":"3","key":"10.1016\/B978-044450813-3\/50030-8_rf0280","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1016\/S0747-7171(86)80028-1","article-title":"A Structure Preserving Clause Form Translation","volume":"2","author":"Plaisted","year":"1986","journal-title":"Journal of Symbolic Computation"},{"key":"10.1016\/B978-044450813-3\/50030-8_bb0275","doi-asserted-by":"crossref","first-page":"102","DOI":"10.1111\/j.1755-2567.1960.tb00558.x","article-title":"An improved proof procedure","volume":"26","author":"Prawitz","year":"1960","journal-title":"Theoria"},{"key":"10.1016\/B978-044450813-3\/50030-8_bb0280","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1007\/BF00243790","article-title":"Adding Equality to Semantic Tableaux","volume":"3","author":"Reeves","year":"1987","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/B978-044450813-3\/50030-8_bb0285","article-title":"Efficient Theorem Provers based on an Abstract Machine","author":"Schumann","year":"1991","journal-title":"PhD thesis, Technische Universit\u00e4t M\u00fcnchen"},{"key":"10.1016\/B978-044450813-3\/50030-8_bb0290","series-title":"Proceedings, 10th International Conference on Automated Deduction (CADE-10)","first-page":"40","article-title":"PARTHEO: A High-Performance Parallel Theorem Prover","author":"Schumann","year":"1990"},{"key":"10.1016\/B978-044450813-3\/50030-8_bb0295","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1016\/0004-3702(76)90021-7","article-title":"Refutation Graphs","volume":"7","author":"Shostak","year":"1976","journal-title":"Artificial Intelligence"},{"key":"10.1016\/B978-044450813-3\/50030-8_bb0300","series-title":"Automation of Reasoning","year":"1983"},{"key":"10.1016\/B978-044450813-3\/50030-8_bb0305","series-title":"First-Order Logic","author":"Smullyan","year":"1968"},{"key":"10.1016\/B978-044450813-3\/50030-8_bb0310","series-title":"1984 International Symposium on Logic Programming","article-title":"A Prolog Technology Theorem Prover","author":"Stickel","year":"1984"},{"key":"10.1016\/B978-044450813-3\/50030-8_bb0315","series-title":"9th International Conference on Automated Deduction (CADE-9)","first-page":"752","article-title":"A Prolog Technology Theorem Prover","author":"Stickel","year":"1988"},{"key":"10.1016\/B978-044450813-3\/50030-8_bb0320","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1016\/0304-3975(92)90168-F","article-title":"A Prolog technology theorem prover: a new exposition and implementation in Prolog","volume":"104","author":"Stickel","year":"1992","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/B978-044450813-3\/50030-8_bb0325","article-title":"The CADE-14 ATP System Competition","author":"Sutcliffe","year":"1998","journal-title":"Technical Report JCU-CS-98\/01, Department of Computer Science, James Cook University"},{"key":"10.1016\/B978-044450813-3\/50030-8_bb0330","series-title":"Proceedings, 12th International Conference on Automated Deduction (CADE-12)","first-page":"708","article-title":"The TPTP problem library","author":"Sutcliffe","year":"1994"},{"key":"10.1016\/B978-044450813-3\/50030-8_bb0335","series-title":"Proceedings of the International Conference on Fifth Generation Computer Systems","first-page":"398","article-title":"Hardware Design and Implementation of the Personal Sequential Inference Machine (PSI)","author":"Taki","year":"1984"},{"key":"10.1016\/B978-044450813-3\/50030-8_bb0340","article-title":"On the Complexity of Proofs in Propositional Logics","volume":"8","author":"Tseitin","year":"1970","journal-title":"Seminars in Mathematics"},{"key":"10.1016\/B978-044450813-3\/50030-8_bb0345","series-title":"Expert systems and their applications (Proceedings)","first-page":"1025","article-title":"A New Abstract Prolog Instruction Set","author":"Vlahavas","year":"1987"},{"key":"10.1016\/B978-044450813-3\/50030-8_bb0350","series-title":"Proceedings IEE Colloquium on Advanced Software Technologies for Scheduling","article-title":"Two problems \u2013 two solutions: One system \u2013 ECLiPSe","author":"Wallace","year":"1993"},{"key":"10.1016\/B978-044450813-3\/50030-8_bb0355","article-title":"An Abstract PROLOG Instruction Set","author":"Warren","year":"1983","journal-title":"Technical Report 309, Artificial Intelligence Center, Computer Science and Technology Division, SRI International, Menlo Park, CA"},{"key":"10.1016\/B978-044450813-3\/50030-8_bb0360","first-page":"1965","article-title":"Combining superposition, sorts and splitting","volume":"Vol. II","author":"Weidenbach","year":"2001"}],"container-title":["Handbook of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:B9780444508133500308?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:B9780444508133500308?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,1,6]],"date-time":"2019-01-06T19:25:37Z","timestamp":1546802737000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/B9780444508133500308"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9780444508133"],"references-count":73,"URL":"https:\/\/doi.org\/10.1016\/b978-044450813-3\/50030-8","relation":{},"subject":[],"published":{"date-parts":[[2001]]}}}