{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,1]],"date-time":"2026-04-01T14:30:12Z","timestamp":1775053812296,"version":"3.50.1"},"reference-count":110,"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\/50006-0","type":"book-chapter","created":{"date-parts":[[2007,6,11]],"date-time":"2007-06-11T13:04:11Z","timestamp":1181567051000},"page":"179-272","source":"Crossref","is-referenced-by-count":34,"title":["The Inverse Method"],"prefix":"10.1016","author":[{"given":"Anatoli","family":"Degtyarev","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrei","family":"Voronkov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/B978-044450813-3\/50006-0_bb0010","first-page":"965","article-title":"Classical type theory","volume":"Vol. II","author":"Andrews","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0015","series-title":"Formal Methods and Semantics","first-page":"493","article-title":"Logic programming","volume":"Vol. B","author":"Apt","year":"1990"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0020","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/BF00302639","article-title":"Strategies for modal resolution: Results and problems","volume":"6","author":"Auffray","year":"1990","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0025","first-page":"445","article-title":"Unification theory","volume":"Vol. I","author":"Baader","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0030","first-page":"273","article-title":"Normal form transformations","volume":"Vol. I","author":"Baaz","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0035","first-page":"1355","article-title":"Automated deduction for many-valued logics","volume":"Vol. II","author":"Baaz","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50006-0_rf0040","first-page":"19","article-title":"Resolution theorem proving","volume":"Vol. I","author":"Bachmair","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0045","first-page":"1149","article-title":"Proof-assistants using dependent type systems","volume":"Vol. II","author":"Barendregt","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0050","article-title":"Semantic construction of intuitionistic logic","author":"Beth","year":"1956","journal-title":"Noord-Hollandsche Uitgevers Maatschappij"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0055","first-page":"749","article-title":"Solving numerical constraints","volume":"Vol. I","author":"Bockmayr","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0060","series-title":"The Classical Decision Problem","author":"B\u00f6rger","year":"1997"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0065","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-015-7642-0","article-title":"Model Theory for Modal Logic","author":"Bowen","year":"1979"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0070","series-title":"Proc. 10th CADE","first-page":"558","article-title":"Minimizing the number of clauses by renaming","author":"Boy de la Tour","year":"1990"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0075","first-page":"845","article-title":"The automation of proof by mathematical induction","volume":"Vol. I","author":"Bundy","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0080","first-page":"1581","article-title":"Reasoning in expressive description logics","volume":"Vol. II","author":"Calvanese","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0085","series-title":"Modal Logic","author":"Chagrov","year":"1996"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0090","first-page":"705","article-title":"Automated reasoning in geometry","volume":"Vol. I","author":"Chou","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0095","first-page":"1635","article-title":"Model checking","volume":"Vol. II","author":"Clarke","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0100","first-page":"913","article-title":"Inductionless induction","volume":"Vol. I","author":"Comon","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0105","series-title":"Foundations of Mathematical Logic","author":"Curry","year":"1963"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0110","first-page":"3","article-title":"The early history of automated deduction","volume":"Vol. I","author":"Davis","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0115","first-page":"8","article-title":"A computer algorithm of establishing deducibility based on the inverse method","volume":"16","author":"Davydov","year":"1969","journal-title":"Zapiski Nauchnyh Seminarov LOMI"},{"issue":"3","key":"10.1016\/B978-044450813-3\/50006-0_bb0120","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1093\/jigpal\/8.3.265","article-title":"Resolution-based methods for modal logics","volume":"8","author":"de Nivelle","year":"2000","journal-title":"Logic Journal of the IGPL"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0125","article-title":"Equality elimination for semantic tableaux","author":"Degtyarev","year":"1994","journal-title":"UPMAIL Technical Report 90, Uppsala University, Computing Science Department"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0130","article-title":"Equality elimination for the inverse method and extension procedures","author":"Degtyarev","year":"1994","journal-title":"UPMAIL Technical Report 92, Uppsala University, Computing Science Department"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0135","series-title":"Proc. International Joint Conference on Artificial Intelligence (IJCAI)","first-page":"342","article-title":"Equality elimination for the inverse method and extension procedures","author":"Degtyarev","year":"1995"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0140","series-title":"Design and Implementation of Symbolic Computation Systems. International Symposium, DISCO'96","first-page":"46","article-title":"Equality elimination for the tableau method","author":"Degtyarev","year":"1996"},{"issue":"1\u20132","key":"10.1016\/B978-044450813-3\/50006-0_bb0145","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1016\/0304-3975(96)00092-8","article-title":"The undecidability of simultaneous rigid E-unification","volume":"166","author":"Degtyarev","year":"1996","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/B978-044450813-3\/50006-0_rf0150","series-title":"Logics in Artificial Intelligence. European Workshop, JELIA'96","first-page":"50","article-title":"What you always wanted to know about rigid E-unification","author":"Degtyarev","year":"1996"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0155","first-page":"609","article-title":"Equality reasoning in sequent-based calculi","volume":"Vol. I","author":"Degtyarev","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0160","first-page":"179","article-title":"The inverse method","volume":"Vol. I","author":"Degtyarev","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0165","first-page":"533","article-title":"Rewriting","volume":"Vol. I","author":"Dershowitz","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0170","first-page":"1241","article-title":"Nonmonotonic reasoning: Towards efficient calculi and implementations","volume":"Vol. II","author":"Dix","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0175","first-page":"1009","article-title":"Higher-order unification and matching","volume":"Vol. II","author":"Dowek","year":"2001"},{"issue":"3","key":"10.1016\/B978-044450813-3\/50006-0_bb0180","doi-asserted-by":"crossref","first-page":"795","DOI":"10.2307\/2275431","article-title":"Contraction-free sequent calculi for intuitionistic logic","volume":"57","author":"Dyckhoff","year":"1992","journal-title":"Journal of Symbolic Logic"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0185","first-page":"1791","article-title":"Resolution decision procedures","volume":"Vol. II","author":"Ferm\u00fcller","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0190","series-title":"Proof methods for modal and intuitionistic logics, Vol. 169 of Synthese Library","author":"Fitting","year":"1983"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0195","series-title":"First Order Logic and Automated Theorem Proving","author":"Fitting","year":"1996"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0200","series-title":"First-Order Modal Logic","author":"Fitting","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0205","series-title":"Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2000)","first-page":"220","article-title":"Term-modal logics","author":"Fitting","year":"2000"},{"key":"10.1016\/B978-044450813-3\/50006-0_rf0210","doi-asserted-by":"crossref","first-page":"176","DOI":"10.1007\/BF01201353","article-title":"Untersuchungen \u00fcber das logische Schlie\u00dfen","volume":"39","author":"Gentzen","year":"1934","journal-title":"Mathematical Zeitschrift"},{"key":"10.1016\/B978-044450813-3\/50006-0_rf0215","doi-asserted-by":"crossref","first-page":"405","DOI":"10.1007\/BF01201363","article-title":"Untersuchungen \u00fcber das logische Schlie\u00dfen","volume":"39","author":"Gentzen","year":"1934","journal-title":"Mathematical Zeitschrift"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0215","series-title":"The Collected Papers of Gerhard Gentzen","first-page":"68","article-title":"Investigations into logical deduction","author":"Gentzen","year":"1969"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0220","series-title":"Proofs and types","author":"Girard","year":"1989"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0225","series-title":"AI*IA 99: Advanced in Artificial Intelligence. 6th Congress of the Italian Association for Artificial Intelligence","first-page":"95","article-title":"The SAT-based approach for classical modal logics","author":"Giunchiglia","year":"2000"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50006-0_bb0230","first-page":"47","article-title":"Predicate and set-theoretic calculi based on logic without the contraction rule","volume":"45","author":"Grishin","year":"1981","journal-title":"Izvestiya Akad. Nauk SSSR"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0235","first-page":"100","article-title":"Tableaux and related methods","volume":"Vol. I","author":"H\u00e4hnle","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0240","first-page":"7","article-title":"Form and content in quantification theory","volume":"8","author":"Hintikka","year":"1955","journal-title":"Acta Philosophica Fennica"},{"issue":"3","key":"10.1016\/B978-044450813-3\/50006-0_bb0245","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1093\/logcom\/9.3.267","article-title":"Optimising description logic subsumption","volume":"9","author":"Horrocks","year":"1999","journal-title":"Journal of Logic and Computation"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50006-0_bb0250","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1093\/logcom\/3.1.63","article-title":"An O(n log n)-space decision procedure for intuitionistic propositional logic","volume":"3","author":"Hudelmaier","year":"1993","journal-title":"Journal of Logic and Computation"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0255","series-title":"Provability in Logic, Vol. 1 of Studies in Philosophy","author":"Kanger","year":"1957"},{"key":"10.1016\/B978-044450813-3\/50006-0_rf0265","series-title":"Computer Programming and Formal Systems","first-page":"87","article-title":"A simplified proof method for elementary logic","author":"Kanger","year":"1963"},{"key":"10.1016\/B978-044450813-3\/50006-0_rf0270","series-title":"Automation of Reasoning. Classical Papers on Computational Logic","first-page":"364","article-title":"A simplified proof method for elementary logic","author":"Kanger","year":"1983"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0265","series-title":"Automation of Reasoning. Classical Papers on Computational Logic","first-page":"364","article-title":"A simplified proof method for elementary logic","author":"Kanger","year":"1983"},{"issue":"3","key":"10.1016\/B978-044450813-3\/50006-0_bb0270","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1016\/0304-3975(84)90047-1","article-title":"A decidable fragment of predicate calculus","volume":"32","author":"Ketonen","year":"1984","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0275","first-page":"11","article-title":"Permutability of inferences in Gentzen's calculi LK and LJ","volume":"10","author":"Kleene","year":"1952","journal-title":"Memoirs of the American Mathematical Society"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0280","series-title":"Mathematical Logic","author":"Kleene","year":"1967"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0285","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\/50006-0_bb0290","first-page":"83","article-title":"Semantical considerations on modal logics","author":"Kripke","year":"1963","journal-title":"Acta Philosophica Fennica, Modal and Many-Valued Logics"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0295","series-title":"Machine Intelligence","first-page":"73","article-title":"A note on the relation between resolution and Maslov's inverse method","author":"Kuechner","year":"1971"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0300","first-page":"2015","article-title":"Model elimination and connection tableau procedures","volume":"Vol. II","author":"Letz","year":"2001"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50006-0_bb0305","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/BF00245018","article-title":"What is the inverse method?","volume":"5","author":"Lifschitz","year":"1989","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0310","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1017\/S0027763000018055","article-title":"Eine Darstellung der intuitionistischen Logik in der klassischen","volume":"1954","author":"Maehara","year":"1954","journal-title":"Nagoya Math. J."},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0315","first-page":"1420","article-title":"The inverse method of establishing deducibility in the classical predicate calculus","volume":"5","author":"Maslov","year":"1964","journal-title":"Soviet Mathematical Doklady"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50006-0_bb0320","first-page":"17","article-title":"An application of the inverse method to the theory of decidable fragments of the classical calculus","volume":"159","author":"Maslov","year":"1966","journal-title":"Soviet Mathematical Doklady"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50006-0_rf0335","first-page":"22","article-title":"An inverse method for establishing deducibility of nonprenex formulas of the predicate calculus","volume":"172","author":"Maslov","year":"1967","journal-title":"Soviet Mathematical Doklady"},{"key":"10.1016\/B978-044450813-3\/50006-0_rf0340","series-title":"Automation of Reasoning (Classical papers on Computational Logic)","first-page":"48","article-title":"An inverse method for establishing deducibility of nonprenex formulas of the predicate calculus","author":"Maslov","year":"1983"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0330","first-page":"26","article-title":"The inverse method of establishing deducibility of logical calculi","volume":"Vol. 98","author":"Maslov","year":"1968"},{"key":"10.1016\/B978-044450813-3\/50006-0_rf0350","article-title":"Relationship betweentactics of the inverse method and the resolution method","volume":"16","author":"Maslov","year":"1969","journal-title":"Zapiski Nauchnyh Seminarov LOMI"},{"key":"10.1016\/B978-044450813-3\/50006-0_rf0355","series-title":"Automation of Reasoning (Classical papers on Computational Logic)","article-title":"Relationship between tactics of the inverse method and the resolution method","author":"Maslov","year":"1983"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0340","first-page":"80","article-title":"The generalization of the inverse method to predicate calculus with equality","volume":"20","author":"Maslov","year":"1971","journal-title":"Zapiski Nauchnyh Seminarov LOMI"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0345","series-title":"Machine Intelligence","first-page":"77","article-title":"Proof-search strategies for methods of the resolution type","author":"Maslov","year":"1971"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0350","series-title":"Automation of Reasoning (Classical papers on Computational Logic)","first-page":"48","article-title":"An inverse method for establishing deducibility of nonprenex formulas of the predicate calculus","author":"Maslov","year":"1983"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0355","series-title":"Mathematical Logic and Automatic Theorem Proving","first-page":"327","article-title":"On strategies of resolution and of the inverse method","author":"Maslov","year":"1983"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0360","series-title":"Automation of Reasoning (Classical papers on Computational Logic)","first-page":"264","article-title":"Relationship between tactics of the inverse method and the resolution method","author":"Maslov","year":"1983"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0365","series-title":"Mathematical Logic and Automatic Theorem Proving","first-page":"291","article-title":"The proof-search theory and the inverse method","author":"Maslov","year":"1983"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0370","series-title":"Automation of Reasoning (Classical papers on Computational Logic)","first-page":"29","article-title":"Mechanical proof-search and the theory of logical deduction in the USSR","author":"Maslov","year":"1983"},{"key":"10.1016\/B978-044450813-3\/50006-0_rf0395","series-title":"9th Soviet Symp. on Cybernetics","first-page":"34","article-title":"Resolution calculi for the non-classical logics","author":"Mints","year":"1981"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0380","series-title":"COLOG-88","first-page":"198","article-title":"Gentzen-type systems and resolution rules. Part I. Propositional logic","author":"Mints","year":"1990"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0385","series-title":"Proc. ASL Summer Meeting, Logic Colloquium'90","first-page":"163","article-title":"Gentzen-type systems and resolution rule, Part II: Predicate logic","author":"Mints","year":"1993"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0390","doi-asserted-by":"crossref","first-page":"58","DOI":"10.1007\/BF01051768","article-title":"Resolution calculus for the first order linear logic","volume":"2","author":"Mints","year":"1993","journal-title":"Journal of Logic, Language and Information"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0395","series-title":"Constraint Programming","first-page":"289","article-title":"Resolution strategies for the intuitionistic logic","author":"Mints","year":"1994"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0400","series-title":"\u2018Proof Theory of Modal Logic\u2019, Studies in Pure and Applied Logic","article-title":"Transfer of sequent calculus strategies to resolution for S4","author":"Mints","year":"1996"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0405","first-page":"371","article-title":"Paramodulation-based theorem proving","volume":"Vol. I","author":"Nieuwenhuis","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0410","series-title":"Automated Deduction \u2014 CADE-15. 15th International Conference on Automated Deduction","first-page":"397","article-title":"On generating small clause normal forms","author":"Nonnengart","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0415","first-page":"335","article-title":"Computing small clause normal forms","volume":"Vol. I","author":"Nonnengart","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0420","first-page":"1403","article-title":"Encoding two-valued nonclassical logics in classical logic","volume":"Vol. II","author":"Ohlbach","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0425","series-title":"Mathematical Logic and Automatic Theorem Proving","first-page":"314","article-title":"The British museum algorithm may be more efficient than resolution","author":"Orevkov","year":"1983"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0430","series-title":"Logic and Computer Science","first-page":"361","article-title":"Isabelle: The next 700 theorem provers","author":"Paulson","year":"1990"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0435","first-page":"1063","article-title":"Logical frameworks","volume":"Vol. II","author":"Pfenning","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0440","first-page":"416","article-title":"On a variant of the constructive predicate calculus without structural deduction rules","volume":"6","author":"Pliu\u0161kevi\u010dius","year":"1965","journal-title":"Soviet Mathematical Doklady"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0445","first-page":"1853","article-title":"Term indexing","volume":"Vol. II","author":"Ramakrishnan","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0450","series-title":"11th International Conference on Automated Deduction","first-page":"522","article-title":"Proof search in the intuitionistic sequent calculus","author":"Shankar","year":"1992"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0455","series-title":"First-Order Logic","author":"Smullyan","year":"1968"},{"issue":"3","key":"10.1016\/B978-044450813-3\/50006-0_bb0460","doi-asserted-by":"crossref","first-page":"273","DOI":"10.1007\/BF00885763","article-title":"Proof strategies in linear logic","volume":"12","author":"Tammet","year":"1994","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0465","series-title":"Automated Deduction \u2014 CADE-13","first-page":"2","article-title":"A resolution theorem prover for intuitionistic logic","author":"Tammet","year":"1996"},{"key":"10.1016\/B978-044450813-3\/50006-0_rf0490","series-title":"Computational Logic and Proof Theory. 5th Kurt G\u00f6del Colloquium, KGC'97","first-page":"65","article-title":"Resolution, inverse method and the sequent calculus","author":"Tammet","year":"1997"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0475","series-title":"Basic Proof Theory, Vol. 43 of Cambridge Tracts in Theoretical Computer Science","author":"Troelstra","year":"1996"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0480","article-title":"A proof search method","author":"Voronkov","year":"1985"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0485","series-title":"COLOG'88","first-page":"327","article-title":"A proof-search method for the first order logic","author":"Voronkov","year":"1990"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0490","series-title":"11th International Conference on Automated Deduction","first-page":"648","article-title":"Theorem proving in non-standard logics based on the inverse method","author":"Voronkov","year":"1992"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0495","doi-asserted-by":"crossref","first-page":"205","DOI":"10.1023\/A:1005934721802","article-title":"Proof-search in intuitionistic logic with equality, or back to simultaneous rigid E-unification","volume":"21","author":"Voronkov","year":"1998","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0500","series-title":"Automated Deduction\u2014CADE-16. 16th International Conference on Automated Deduction","first-page":"383","article-title":"KK: a theorem prover for K","author":"Voronkov","year":"1999"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0505","series-title":"Principles of Knowledge Representation and Reasoning (KR'2000)","first-page":"198","article-title":"How to decide K using K","author":"Voronkov","year":"2000"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0510","series-title":"LICS'2000","article-title":"How to optimize proof-search in modal logics: a new way of proving redundancy criteria for sequent calculi","author":"Voronkov","year":"2000"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0515","doi-asserted-by":"crossref","DOI":"10.1145\/371316.371511","article-title":"How to optimize proof-search in modal logics: new methods of proving redundancy criteria for sequent calculi","author":"Voronkov","year":"2001","journal-title":"ACM Transactions on Computational Logic"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0520","first-page":"1487","article-title":"Connections in nonclassical logics","volume":"Vol. II","author":"Waaler","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0525","first-page":"1965","article-title":"Combining superposition, sorts and splitting","volume":"Vol. II","author":"Weidenbach","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50006-0_bb0530","series-title":"Automated Deduction \u2014 CADE-13","first-page":"141","article-title":"SPASS & FLOTTER. Version 0.42","author":"Weidenbach","year":"1996"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50006-0_bb0535","doi-asserted-by":"crossref","first-page":"165","DOI":"10.1016\/0168-0072(89)90053-5","article-title":"Maslov's inverse method and decidable classes","volume":"42","author":"Zamov","year":"1989","journal-title":"Annals of Pure and Applied Logic"}],"container-title":["Handbook of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:B9780444508133500060?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:B9780444508133500060?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,4,29]],"date-time":"2019-04-29T00:54:35Z","timestamp":1556499275000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/B9780444508133500060"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9780444508133"],"references-count":110,"URL":"https:\/\/doi.org\/10.1016\/b978-044450813-3\/50006-0","relation":{},"subject":[],"published":{"date-parts":[[2001]]}}}