{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T19:49:04Z","timestamp":1762458544174,"version":"build-2065373602"},"reference-count":153,"publisher":"Elsevier","isbn-type":[{"type":"print","value":"9780444508133"}],"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\/50005-9","type":"book-chapter","created":{"date-parts":[[2007,6,11]],"date-time":"2007-06-11T13:04:11Z","timestamp":1181567051000},"page":"101-178","source":"Crossref","is-referenced-by-count":48,"title":["Tableaux and Related Methods"],"prefix":"10.1016","author":[{"given":"Reiner","family":"H\u00e4hnle","sequence":"first","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/B978-044450813-3\/50005-9_bb0010","first-page":"97","article-title":"Integration of automated and interactive theorem proving","volume":"Vol. II","author":"Ahrendt","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0015","doi-asserted-by":"crossref","first-page":"414","DOI":"10.2307\/2269949","article-title":"Resolution in type theory","volume":"36","author":"Andrews","year":"1971","journal-title":"Journal of Symbolic Logic"},{"issue":"8","key":"10.1016\/B978-044450813-3\/50005-9_bb0020","doi-asserted-by":"crossref","first-page":"801","DOI":"10.1109\/TC.1976.1674698","article-title":"Refutations by matings","volume":"C-25","author":"Andrews","year":"1976","journal-title":"IEEE Transactions on Computers"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0025","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":"JACM"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50005-9_bb0030","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1007\/BF00881838","article-title":"Gentzen-type systems, resolution and tableaux","volume":"10","author":"Avron","year":"1993","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0035","first-page":"445","article-title":"Unification theory","volume":"Vol. I","author":"Baader","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0040","first-page":"273","article-title":"Normal form transformations","volume":"Vol. I","author":"Baaz","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0045","first-page":"217","article-title":"Nonelementary speedups between different versions of tableaux","author":"Baaz","year":"1995"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0050","first-page":"1355","article-title":"Automated deduction for many-valued logics","volume":"Vol. II","author":"Baaz","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0055","first-page":"19","article-title":"Resolution theorem proving","volume":"Vol. I","author":"Bachmair","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0060","first-page":"60","article-title":"Hyper Tableaux \u2014 The Next Generation","author":"Baumgartner","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0065","series-title":"Proc. 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\/50005-9_bb0070","series-title":"Intellectics and Computational Logic \u2014 Papers in Honor of Wolfgang Bibel","article-title":"A confluent connection calculus","author":"Baumgartner","year":"2000"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0075","doi-asserted-by":"crossref","first-page":"445","DOI":"10.1006\/jsco.1993.1058","article-title":"Consolution as a framework for comparing calculi","volume":"16","author":"Baumgartner","year":"1993","journal-title":"Journal of Symbolic Computation"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0080","doi-asserted-by":"crossref","first-page":"339","DOI":"10.1007\/BF00881948","article-title":"Model Elimination without Contrapositives and its Application to PTTP","volume":"13","author":"Baumgartner","year":"1994","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0085","series-title":"Proc. International Workshop on First Order Theorem Proving","article-title":"Refinements for Restart Model Elimination","author":"Baumgartner","year":"1997"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0090","first-page":"73","article-title":"Variants of clausal tableaux","volume":"Vol. 1","author":"Baumgartner","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0095","series-title":"Proc. European Workshop: Logics in Artificial Intelligence, JELIA","first-page":"1","article-title":"Hyper tableaux","volume":"Vol. 1126","author":"Baumgartner","year":"1996"},{"issue":"1\u20132","key":"10.1016\/B978-044450813-3\/50005-9_bb0100","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1016\/S0004-3702(96)00042-2","article-title":"Computing answers with model elimination","volume":"90","author":"Baumgartner","year":"1997","journal-title":"Artificial Intelligence Journal"},{"year":"1998","author":"Beckert","series-title":"Integrating and Unifying Methods of Tableau-based Theorem Proving","key":"10.1016\/B978-044450813-3\/50005-9_rf0105"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0110","series-title":"Proc. Third Int. Workshop on First-Order Theorem Proving (FTP), St. Andrews, Scotland","first-page":"44","article-title":"Depth-first proof search without backtracking for free-variable clausal tableaux","author":"Beckert","year":"2000"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0115","series-title":"Proc. International Conference on Theorem Proving with Analytic Tableaux and Related Methods, Pont-a-Mousson, France","first-page":"91","article-title":"Free variable tableaux for propositional modal logics","author":"Beckert","year":"1997"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0120","first-page":"11","article-title":"Analytic tableaux","volume":"Vol. I","author":"Beckert","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0125","series-title":"Proc. 13th Conference on Automated Deduction, New Brunswick\/NJ, USA","first-page":"303","article-title":"The tableau-based theorem prover 3TAP, version 4.0","author":"Beckert","year":"1996"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0130","first-page":"108","article-title":"The even more liberalized \u03b4-rule in free variable semantic tableaux","volume":"Vol. 713","author":"Beckert","year":"1993"},{"issue":"3","key":"10.1016\/B978-044450813-3\/50005-9_bb0135","doi-asserted-by":"crossref","first-page":"339","DOI":"10.1007\/BF00881804","article-title":"leanTAP: Lean tableau-based deduction","volume":"15","author":"Beckert","year":"1995","journal-title":"Journal of Automated Reasoning"},{"year":"1986","series-title":"Logik-Texte. Kommentierte Auswahl zur Geschichte der modernen Logik","key":"10.1016\/B978-044450813-3\/50005-9_bb0140"},{"issue":"13","key":"10.1016\/B978-044450813-3\/50005-9_bb0145","first-page":"309","article-title":"Semantic entailment and formal derivability","volume":"18","author":"Beth","year":"1955","journal-title":"Mededelingen van de Koninklijke Nederlandse Akademie van Wetenschappen, Afdeling Letterkunde, N.R."},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0150","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1016\/0304-3975(79)90054-9","article-title":"Tautology testing with a generalized matrix method","volume":"8","author":"Bibel","year":"1979","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0155","doi-asserted-by":"crossref","first-page":"633","DOI":"10.1145\/322276.322277","article-title":"On matrices with connections","volume":"28","author":"Bibel","year":"1981","journal-title":"JACM"},{"year":"1982","author":"Bibel","series-title":"Automated Theorem Proving","key":"10.1016\/B978-044450813-3\/50005-9_bb0160"},{"issue":"3","key":"10.1016\/B978-044450813-3\/50005-9_bb0165","doi-asserted-by":"crossref","first-page":"269","DOI":"10.1016\/0004-3702(82)90024-8","article-title":"A comparative study of several proof procedures","volume":"18","author":"Bibel","year":"1982","journal-title":"Artificial Intelligence"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0170","series-title":"Logic Colloquium '81","first-page":"11","article-title":"Computationally improved versions of herbrand's theorem","author":"Bibel","year":"1982"},{"year":"1987","author":"Bibel","series-title":"Automated Theorem Proving","key":"10.1016\/B978-044450813-3\/50005-9_bb0175"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0180","first-page":"1","article-title":"Issues in theorem proving based on the connection method","volume":"Vol. 918","author":"Bibel","year":"1995"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0185","first-page":"67","article-title":"Methods and calculi for deduction","volume":"Vol. 1","author":"Bibel","year":"1992"},{"year":"1998","series-title":"Automated Deduction: A Basis for Applications","key":"10.1016\/B978-044450813-3\/50005-9_bb0190"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0195","series-title":"International Computing Symposium","first-page":"205","article-title":"Proof search in a Gentzen-like system of first-order logic","author":"Bibel","year":"1975"},{"issue":"3","key":"10.1016\/B978-044450813-3\/50005-9_bb0200","doi-asserted-by":"crossref","first-page":"281","DOI":"10.1016\/S0004-3702(78)80017-4","article-title":"Towards the automation of set theory and its logic","volume":"10","author":"Brown","year":"1978","journal-title":"Artificial Intelligence"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0205","first-page":"122","article-title":"A deduction method complete for refutation and finite satisfiability","volume":"Vol. 1489","author":"Bry","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50005-9_rf0210","first-page":"143","article-title":"Minimal model generation with positive unit hyper-resolution tableaux","volume":"Vol. 1071","author":"Bry","year":"1996"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0215","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","article-title":"Graph-based algorithms for Boolean function manipulation","volume":"C-35","author":"Bryant","year":"1986","journal-title":"IEEE Transactions on Computers"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0220","series-title":"Proc. Second Int. Workshop on First-Order Theorem Proving, FTP'98","first-page":"86","article-title":"A further and effective liberalization of the delta-rule in free variable semantic tableaux","author":"Cantone","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0225","doi-asserted-by":"crossref","first-page":"36ff","DOI":"10.2307\/2273702","article-title":"The relative efficiency of propositional proof systems","volume":"44","author":"Cook","year":"1979","journal-title":"Journal of Symbolic Logic"},{"year":"1990","author":"D'Agostino","article-title":"Investigations into the Complexity of some Propositional Calculi","key":"10.1016\/B978-044450813-3\/50005-9_bb0230"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0235","doi-asserted-by":"crossref","first-page":"235","DOI":"10.1007\/BF00156916","article-title":"Are tableaux an improvement on truth tables? Cut-free proofs and bivalence","volume":"1","author":"D'Agostino","year":"1992","journal-title":"Journal of Logic, Language and Information"},{"year":"1999","series-title":"Handbook of Tableau Methods","key":"10.1016\/B978-044450813-3\/50005-9_bb0240"},{"issue":"3","key":"10.1016\/B978-044450813-3\/50005-9_bb0245","first-page":"285","article-title":"The taming of the cut","volume":"4","author":"D'Agostino","year":"1994","journal-title":"Journal of Logic and Computation"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0250","first-page":"195","article-title":"Using automated theorem provers in verification of protocols","volume":"Vol. III","author":"Dahn","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0255","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1145\/368273.368557","article-title":"A machine program for theorem-proving","volume":"5","author":"Davis","year":"1962","journal-title":"Communications of the ACM"},{"issue":"3","key":"10.1016\/B978-044450813-3\/50005-9_bb0260","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1145\/321033.321034","article-title":"A computing procedure for quantification theory","volume":"7","author":"Davis","year":"1960","journal-title":"JACM"},{"key":"10.1016\/B978-044450813-3\/50005-9_rf0265","doi-asserted-by":"crossref","first-page":"12","DOI":"10.1007\/BF01117463","article-title":"Synthesis of the resolution method with the inverse method","volume":"1","author":"Davydov","year":"1973","journal-title":"Journal of Soviet Mathematics"},{"volume":"vol. 20","year":"1971","first-page":"24","key":"10.1016\/B978-044450813-3\/50005-9_rf3000"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50005-9_bb0270","doi-asserted-by":"crossref","first-page":"47","DOI":"10.1023\/A:1005996623714","article-title":"What you always wanted to know about rigid E-unification","volume":"20","author":"Degtyarev","year":"1998","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0275","first-page":"609","article-title":"Equality reasoning in sequent-based calculi","volume":"Vol. I","author":"Degtyarev","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0280","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1016\/0743-1066(84)90014-1","article-title":"Linear-time algorithms for testing the satisfiability of propositional Horn formul\u02e6","volume":"3","author":"Dowling","year":"1984","journal-title":"Journal of Logic Programming"},{"year":"1992","author":"Eder","series-title":"Relative Complexities of First-Order Calculi","key":"10.1016\/B978-044450813-3\/50005-9_bb0285"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0290","first-page":"158","article-title":"Non-elementary speed-ups in proof length by different variants of classical analytic calculi","volume":"Vol. 1227","author":"Egly","year":"1997"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0295","first-page":"1","article-title":"Introduction","author":"Fitting","year":"1999"},{"year":"1990","author":"Fitting","series-title":"First-Order Logic and Automated Theorem Proving","key":"10.1016\/B978-044450813-3\/50005-9_bb0300"},{"year":"1996","author":"Fitting","series-title":"First-Order Logic and Automated Theorem Proving","key":"10.1016\/B978-044450813-3\/50005-9_bb0305"},{"key":"10.1016\/B978-044450813-3\/50005-9_rf0310","series-title":"Proceedings 8th International Conference on Logic Programming, Paris\/France","first-page":"535","article-title":"A model generation theorem prover in KL1 using a ramified-stack algorithm","author":"Fujita","year":"1991"},{"issue":"4","key":"10.1016\/B978-044450813-3\/50005-9_bb0315","doi-asserted-by":"crossref","first-page":"251","DOI":"10.1016\/S0743-1066(85)80003-0","article-title":"N-Prolog: An extension of Prolog with hypothetical implication II\u2014logical foundations, and negation as failure","volume":"2","author":"Gabbay","year":"1985","journal-title":"Journal of Logic Programming"},{"issue":"4","key":"10.1016\/B978-044450813-3\/50005-9_bb0320","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1016\/0743-1066(84)90029-3","article-title":"N-Prolog: An extension of Prolog with hypothetical implications I","volume":"1","author":"Gabbay","year":"1984","journal-title":"Journal of Logic Programming"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50005-9_bb0325","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1016\/0743-1066(89)90009-5","article-title":"Algorithms for testing the satisfiability of propositional formulae","volume":"7","author":"Gallo","year":"1989","journal-title":"Journal of Logic Programming"},{"year":"1979","author":"Garey","series-title":"Computers and Intractability","key":"10.1016\/B978-044450813-3\/50005-9_bb0330"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0335","doi-asserted-by":"crossref","first-page":"176","DOI":"10.1007\/BF01201353","article-title":"Untersuchungen \u00fcber das Logische Schliessen","volume":"39","author":"Gentzen","year":"1935","journal-title":"Mathematische Zeitschrift"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0340","series-title":"Proc. Third Int. Workshop on First-Order Theorem Proving, St. Andrews, Scotland","first-page":"227","article-title":"Proof search without backtracking using instance streams, position paper","author":"Giese","year":"2000"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0345","series-title":"Proc. International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, Saratoga Springs\/NY, USA, number 1617 in 'LNCS'","first-page":"171","article-title":"Hilbert's \u03b5-terms in automated theorem proving","author":"Giese","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0350","series-title":"Handbook of Tableau Methods","first-page":"529","article-title":"Tableaux for many-valued logics","author":"H\u00e4hnle","year":"1999"},{"issue":"6","key":"10.1016\/B978-044450813-3\/50005-9_bb0355","doi-asserted-by":"crossref","first-page":"819","DOI":"10.1093\/logcom\/6.6.819","article-title":"A-ordered tableaux","volume":"6","author":"H\u00e4hnle","year":"1996","journal-title":"Journal of Logic and Computation"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0360","series-title":"Foundations of Intelligent Systems, 10th International Symposium, ISMIS'97, Charlotte, North Carolina, USA","first-page":"590","article-title":"Completeness for linear regular negation normal form inference systems","author":"H\u00e4hnle","year":"1997"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0365","first-page":"173","article-title":"Ordered tableaux: Extensions and applications","volume":"Vol. 1227","author":"H\u00e4hnle","year":"1997"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0370","first-page":"1","article-title":"MGTP: a model generation theorem prover\u2014its advanced features and applications","volume":"Vol. 1227","author":"Hasegawa","year":"1997"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0375","first-page":"176","article-title":"Non-Horn magic sets to incorporate top-down inference into bottom-up theorem proving","volume":"Vol. 1249","author":"Hasegawa","year":"1997"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0380","series-title":"Proc. 11th International Conference on Automated Deduction","first-page":"776","article-title":"MGTP: A parallel theorem prover based on lazy model generation","author":"Hasegawa","year":"1992"},{"year":"1930","author":"Herbrand","series-title":"Recherches sur la th\u00e9orie de la d\u00e9monstration","key":"10.1016\/B978-044450813-3\/50005-9_bb0385"},{"year":"1971","author":"Herbrand","article-title":"Jacques Herbrand: Logical Writings","key":"10.1016\/B978-044450813-3\/50005-9_bb0390"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0395","first-page":"7","article-title":"Form and content in quantification theory","volume":"8","author":"Hintikka","year":"1955","journal-title":"Acta Philosohica Fennica"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0400","article-title":"Linking BDD-based symbolic evaluation to interactive theorem-proving","author":"Joyce","year":"1993","journal-title":"Technical Report TR-93-18, UBC"},{"volume":"Vol. 1","year":"1957","author":"Kanger","key":"10.1016\/B978-044450813-3\/50005-9_rf0415"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0410","first-page":"708","article-title":"Semantic tableaux with ordering restrictions","author":"Klingenbeck","year":"1994"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0415","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1016\/0004-3702(85)90084-0","article-title":"Depth-first iterative deepening: an optimal admissible tree search","volume":"27","author":"Korf","year":"1985","journal-title":"Artificial Intelligence"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0420","series-title":"Position Papers, International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, Saratoga Springs, NY, USA","first-page":"101","article-title":"A proof of completeness for non-Horn magic sets and its application to proof condensation","author":"Koshimura","year":"1999"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0425","first-page":"569","article-title":"Predicate logic as a programming language","volume":"74","author":"Kowalski","year":"1974","journal-title":"Information Processing"},{"issue":"3","key":"10.1016\/B978-044450813-3\/50005-9_bb0430","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\/50005-9_bb0435","article-title":"First-Order Calculi and Proof Procedures for Automated Deduction","author":"Letz","year":"1993","journal-title":"PhD thesis, TH Darmstadt"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0440","series-title":"Proc. 15th International Conference on Automated Deduction (CADE), Lindau","first-page":"381","article-title":"Using matings for pruning connection tableaux","author":"Letz","year":"1998"},{"issue":"3","key":"10.1016\/B978-044450813-3\/50005-9_bb0445","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"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50005-9_bb0450","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"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0455","first-page":"2015","article-title":"Model elimination and connection tableau procedures","volume":"Vol. II","author":"Letz","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0460","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1007\/BF02120399","article-title":"Wynikanie semantyczne a wynikanie formalne (logical consequence, semantic and formal","volume":"10","author":"Lis","year":"1960","journal-title":"Studia Logica"},{"year":"1987","author":"Lloyd","series-title":"Foundations of Logic Programming","key":"10.1016\/B978-044450813-3\/50005-9_bb0465"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0470","series-title":"Proc. IRIA Symp. Automatic Demonstration","first-page":"147","article-title":"A linear format for resolution","author":"Loveland","year":"1968"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50005-9_bb0475","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\/50005-9_bb0480","doi-asserted-by":"crossref","first-page":"349","DOI":"10.1145\/321526.321527","article-title":"A simplified format for the model elimination procedure","volume":"16","author":"Loveland","year":"1969","journal-title":"Journal of the ACM"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50005-9_bb0485","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"},{"year":"1978","author":"Loveland","article-title":"Automated Theorem Proving. A Logical Basis","key":"10.1016\/B978-044450813-3\/50005-9_bb0490"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0495","series-title":"Proc. Fourth International Conference on Logic Programming, ICLP","first-page":"456","article-title":"Near-Horn PROLOG","author":"Loveland","year":"1987"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0500","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/BF00249353","article-title":"Near-Horn Prolog and beyond","volume":"7","author":"Loveland","year":"1991","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0505","series-title":"Computational Logic: Essays in Honor of Alan Robinson","article-title":"A near-Horn Prolog for compilation","author":"Loveland","year":"1991"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50005-9_bb0510","doi-asserted-by":"crossref","first-page":"325","DOI":"10.1007\/BF00881861","article-title":"SATCHMORE: SATCHMO with Relevancy","volume":"14","author":"Loveland","year":"1995","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/B978-044450813-3\/50005-9_rf0525","series-title":"Proc. IRIA Symp. Automatic Demonstration","first-page":"163","article-title":"Refinements in resolution theory","author":"Luckham","year":"1968"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0520","series-title":"Proceedings 9th Conference on Automated Deduction","first-page":"415","article-title":"SATCHMO: A theorem prover implemented in Prolog","author":"Manthey","year":"1988"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0525","series-title":"Proc. 13th European Conference on Artificial Intelligence, Brighton","first-page":"408","article-title":"Cook and Reckhow are wrong: subexponential proofs for their families of formulae","author":"Massacci","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0530","series-title":"Proc. International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, Oosterwijk, The Netherlands","first-page":"217","article-title":"Simplification: A general constraint propagation technique for propositional and modal tableaux","author":"Massacci","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0535","series-title":"Annali dell' Universit\u00e0 di Ferrara, Nuova Serie, sezione III","article-title":"Classical analytical deduction","author":"Mondadori","year":"1988"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0540","series-title":"Annali dell' Universit\u00e0 di Ferrara, Nuova Serie, sezione III","article-title":"Classical analytical deduction, part II","author":"Mondadori","year":"1989"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0545","series-title":"Annali dell' Universit\u00e0 di Ferrara, Nuova Serie, sezione III","article-title":"An improvement of Jeffrey's deductive trees","author":"Mondadori","year":"1989"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50005-9_bb0550","doi-asserted-by":"crossref","first-page":"237","DOI":"10.1023\/A:1005808119103","article-title":"SETHEO and E-SETHEO\u2014the CADE-13 systems","volume":"18","author":"Moser","year":"1997","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0555","series-title":"Proc. 15th International Conference on Automated Deduction, Lindau, Germany","first-page":"397","article-title":"On generating small clause normal forms","author":"Nonnengart","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0560","first-page":"335","article-title":"Computing small clause normal forms","volume":"Vol. I","author":"Nonnengart","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0565","series-title":"Proc. 15th International Conference on Automated Deduction (CADE), Lindau","first-page":"333","article-title":"On the relationship between non-Horn magic sets and relevancy testing","author":"Ohta","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0570","series-title":"Proc. 8th International Conference on Automated Deduction","first-page":"384","article-title":"Controlling deduction with proof condensation and heuristics","author":"Oppacher","year":"1986"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0575","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1007\/BF00244513","article-title":"HARP: A tableau-based theorem prover","volume":"4","author":"Oppacher","year":"1988","journal-title":"Journal of Automated Reasoning"},{"year":"1996","author":"Pape","series-title":"Vergleich und Analyse von Ordnungseinschr\u00e4nkungen f\u00fcr freie Variablen Tableau","key":"10.1016\/B978-044450813-3\/50005-9_bb0580"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0585","series-title":"Fifth Kurt-G\u00f6del-Colloquium, KGC'97, Vienna","first-page":"219","article-title":"Restart tableaux with selection function","author":"Pape","year":"1997"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0590","series-title":"Proc. Third International Workshop on Extensions of Logic Programming, Bologna","first-page":"1","article-title":"SLWV \u2014 a theorem prover for logic programming","author":"Pereira","year":"1992"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0595","doi-asserted-by":"crossref","first-page":"227","DOI":"10.1016\/0004-3702(82)90041-8","article-title":"A simplified problem reduction format","volume":"18","author":"Plaisted","year":"1982","journal-title":"Artificial Intelligence"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0600","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1007\/BF00244944","article-title":"Non-Horn clause logic programming without contrapositives","volume":"4","author":"Plaisted","year":"1988","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0605","doi-asserted-by":"crossref","first-page":"389","DOI":"10.1007\/BF00244355","article-title":"A sequent-style model elimination strategy and a positive refinement","volume":"6","author":"Plaisted","year":"1990","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/B978-044450813-3\/50005-9_rf0620","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"},{"year":"1997","author":"Plaisted","series-title":"The Efficiency of Theorem Proving Strategies: A Comparative and Asymptotic Analysis","key":"10.1016\/B978-044450813-3\/50005-9_bb0615"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0620","article-title":"Deduktion mit Shannongraphen f\u00fcr Pr\u00e4dikatenlogik erster Stufe","author":"Posegga","year":"1993","journal-title":"PhD thesis, University of Karlsruhe, Diski 51, infix Verlag"},{"issue":"6","key":"10.1016\/B978-044450813-3\/50005-9_bb0625","doi-asserted-by":"crossref","first-page":"697","DOI":"10.1093\/logcom\/5.6.697","article-title":"Deduction with first-order Shannon graphs","volume":"5","author":"Posegga","year":"1995","journal-title":"Journal of Logic and Computation"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0630","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"},{"year":"1998","author":"Preiss","article-title":"Beweisvisualisierung und -analyse mit Hypergraphen","key":"10.1016\/B978-044450813-3\/50005-9_bb0635"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0640","article-title":"Optimization, Hypergraphs and Logical Inference","author":"Rago","year":"1994","journal-title":"PhD thesis, Dipartimento di Informatica, Universit\u00e0 di Pisa, Available as Tech Report TD-4\/94."},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0645","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1016\/0743-1066(92)90038-5","article-title":"A comparison of three Prolog extensions","volume":"12","author":"Reed","year":"1992","journal-title":"Journal of Logic Programming"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0650","series-title":"Technical Report Technical report DUKE-TR-1992-20","article-title":"Near-Horn Prolog and the ancestry family of procedures","author":"Reed","year":"1992"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0655","series-title":"Advances in Artificial Intelligence (Proceedings of AISB-87)","first-page":"125","article-title":"Semantic tableaux as a framework for automated theorem-proving","author":"Reeves","year":"1987"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0660","doi-asserted-by":"crossref","first-page":"630","DOI":"10.1145\/321662.321678","article-title":"Two results on ordering for resolution with merging and linear format","volume":"18","author":"Reiter","year":"1971","journal-title":"Journal of the ACM"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0665","first-page":"227","article-title":"Automatic deduction with hyper-resolution","volume":"1","author":"Robinson","year":"1965","journal-title":"Int. Journal of Computer Math."},{"issue":"1","key":"10.1016\/B978-044450813-3\/50005-9_bb0670","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/321250.321253","article-title":"A machine-oriented logic based on the resolution principle","volume":"12","author":"Robinson","year":"1965","journal-title":"JACM"},{"year":"1960","author":"Sch\u00fctte","series-title":"Beweistheorie, Vol. 103 of Die Grundlehren der mathematischen Wissenschaften in Einzeldarstellungen mit besonderer Ber\u00fccksichtigung der Anwendungsgebiete","key":"10.1016\/B978-044450813-3\/50005-9_bb0675"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50005-9_bb0680","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1023\/A:1008725524946","article-title":"A tutorial on Stlmarck's proof procedure for propositional logic","volume":"16","author":"Sheeran","year":"2000","journal-title":"Formal Methods in Systems Design"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0685","series-title":"Proc. 12th International Conference on Logic Programming","first-page":"249","article-title":"Two approaches for finite-domain constraint satisfaction problemml: CP and MGTP","author":"Shirai","year":"1995"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0690","series-title":"Proc. International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, Pont-\u00e0-Mousson, France","first-page":"328","article-title":"A framework for using knowledge in tableau proofs","author":"Shults","year":"1997"},{"year":"1983","series-title":"Automation of Reasoning: Classical Papers in Computational Logic 1967\u20131970","key":"10.1016\/B978-044450813-3\/50005-9_bb0695"},{"year":"1983","series-title":"Automation of Reasoning: Classical Papers in Computational Logic 1957\u20131966","key":"10.1016\/B978-044450813-3\/50005-9_bb0700"},{"issue":"4","key":"10.1016\/B978-044450813-3\/50005-9_bb0705","doi-asserted-by":"crossref","first-page":"687","DOI":"10.1145\/321420.321428","article-title":"Automatic theorem proving with renamable and semantic resolution","volume":"14","author":"Slagle","year":"1967","journal-title":"Journal of the ACM"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0710","series-title":"Procesdings of the National Academy of Sciences of the U.S.A.","first-page":"828","article-title":"A unifying principle in quantification theory","author":"Smullyan","year":"1963"},{"year":"1995","author":"Smullyan","series-title":"First-Order Logic","key":"10.1016\/B978-044450813-3\/50005-9_bb0715"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50005-9_bb0720","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"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50005-9_rf0735","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1023\/A:1006285423991","article-title":"The CADE-15 ATP system competition","volume":"23","author":"Sutcliffe","year":"1999","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0730","article-title":"The TPTP problem library, TPTP v2.2.0","author":"Suttner","year":"1999","journal-title":"Technical Report JCU-CS-99\/02, Department of Computer Science, James Cook University"},{"year":"1969","series-title":"The Collected Papers of Gerhard Gentzen","key":"10.1016\/B978-044450813-3\/50005-9_bb0735"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0740","series-title":"Proc. 5th International Workshop on Theorem Proving with analytic Tableaux and Related Methods (TABLEAUX), Terrassini, Italy","first-page":"312","article-title":"Proof search in intuitionistic logic based on constraint satisfaction","author":"Voronkov","year":"1996"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0745","series-title":"Proc. 13th IEEE Symposium on Logic in Computer Science, LICS, Indianapolis, USA","first-page":"252","article-title":"Herbrand's theorem, automated reasoning and semantic tableaux","author":"Voronkov","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0750","first-page":"1487","article-title":"Connections in nonclassical logics","volume":"Vol. II","author":"Waaler","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0755","article-title":"Proof Truncation Techniques in Model Elimination Tableaux","author":"Wallace","year":"1994","journal-title":"PhD thesis, University of Newcastle, Australia"},{"issue":"6","key":"10.1016\/B978-044450813-3\/50005-9_bb0760","first-page":"921","article-title":"Regressive merging in model elimination tableau-based theorem provers","volume":"3","author":"Wallace","year":"1995","journal-title":"Journal of the Interest Group in Pure and Applied Logics"},{"key":"10.1016\/B978-044450813-3\/50005-9_bb0765","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:B9780444508133500059?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:B9780444508133500059?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:26:07Z","timestamp":1546802767000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/B9780444508133500059"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9780444508133"],"references-count":153,"URL":"https:\/\/doi.org\/10.1016\/b978-044450813-3\/50005-9","relation":{},"subject":[],"published":{"date-parts":[[2001]]}}}