{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:47:49Z","timestamp":1749124069946},"reference-count":138,"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\/50023-0","type":"book-chapter","created":{"date-parts":[[2007,6,11]],"date-time":"2007-06-11T09:04:11Z","timestamp":1181552651000},"page":"1403-1486","source":"Crossref","is-referenced-by-count":24,"title":["Encoding Two-Valued Nonclassical Logics in Classical Logic"],"prefix":"10.1016","author":[{"given":"Hans J\u00fcrgen","family":"Ohlbach","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andreas","family":"Nonnengart","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Maarten","family":"de Rijke","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dov M.","family":"Gabbay","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"year":"1988","series-title":"Non-Well-Founded Sets","author":"Aczel","key":"10.1016\/B978-044450813-3\/50023-0_bb0010"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0015","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1023\/A:1004275029985","article-title":"Modal languages and bounded fragments of predicate logic","volume":"27","author":"Andr\u00e9ka","year":"1998","journal-title":"Journal of Philosophical Logic"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0020","first-page":"965","article-title":"Classical type theory","volume":"Vol. II","author":"Andrews","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0025","series-title":"Proceedings AiML-ICTL 2000","article-title":"Description and\/or hybrid logic","author":"Areces","year":"2000"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0030","series-title":"Proceedings ECAI-2000","article-title":"Tree-based heuristics for modal theorem proving","author":"Areces","year":"2000"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0035","article-title":"Unification with associative functions","author":"Auer","year":"1992","journal-title":"PhD thesis, Technical University Vienna"},{"issue":"3","key":"10.1016\/B978-044450813-3\/50023-0_bb0040","doi-asserted-by":"crossref","first-page":"247","DOI":"10.1093\/logcom\/2.3.247","article-title":"Modal theorem proving: An equational viewpoint","volume":"2","author":"Auffray","year":"1992","journal-title":"Journal of Logic and Computation"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0045","first-page":"445","article-title":"Unification theory","volume":"Vol. I","author":"Baader","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0050","first-page":"273","article-title":"Normal form transformations","volume":"Vol. I","author":"Baaz","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0055","series-title":"Proceedings LICS'94: Logic in Computer Science","first-page":"213","article-title":"A non-elementary speed up in proof length by structural clause transformation","author":"Baaz","year":"1994"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0060","first-page":"1355","article-title":"Automated deduction for many-valued logics","volume":"Vol. II","author":"Baaz","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0065","first-page":"19","article-title":"Resolution theorem proving","volume":"Vol. I","author":"Bachmair","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0070","first-page":"1149","article-title":"Proof-assistants using dependent type systems","volume":"Vol. II","author":"Barendregt","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50023-0_rf0075","doi-asserted-by":"crossref","first-page":"255","DOI":"10.1023\/A:1008644009416","article-title":"Automata based symbolic reasoning in hardware verification","volume":"13","author":"Basin","year":"1998","journal-title":"Journal of Formal Methods in Systems Design"},{"year":"2001","series-title":"Modal Logic","author":"Blackburn","key":"10.1016\/B978-044450813-3\/50023-0_bb0080"},{"year":"2000","series-title":"Bliksem Version 1.10B","author":"Bli","key":"10.1016\/B978-044450813-3\/50023-0_bb0085"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0090","first-page":"749","article-title":"Solving numerical constraints","volume":"Vol. I","author":"Bockmayr","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0095","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\/50023-0_bb0100","first-page":"1581","article-title":"Reasoning in expressive description logics","volume":"Vol. II","author":"Calvanese","year":"2001"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50023-0_bb0105","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1093\/jigpal\/5.2.287","article-title":"A polynomial translation of S4 into T and contraction-free tableaux for S4","volume":"5","author":"Cerrito","year":"1997","journal-title":"Logic Journal of the IGPL"},{"year":"1980","series-title":"Modal Logic: An Introduction","author":"Chellas","key":"10.1016\/B978-044450813-3\/50023-0_bb0110"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0115","first-page":"705","article-title":"Automated reasoning in geometry","volume":"Vol. I","author":"Chou","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0120","doi-asserted-by":"crossref","first-page":"241","DOI":"10.1016\/0167-6423(83)90017-5","article-title":"Using branching time temporal logic to synthesize synchronization skeletons","volume":"2","author":"Clarke","year":"1982","journal-title":"Science of Computer Programming"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0125","first-page":"1635","article-title":"Model checking","volume":"Vol. II","author":"Clarke","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0130","first-page":"913","article-title":"Inductionless induction","volume":"Vol. I","author":"Comon","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0135","doi-asserted-by":"crossref","first-page":"317","DOI":"10.1007\/BF00881803","article-title":"A set-theoretic translation method for polymodal logics","volume":"15","author":"D'Agostino","year":"1995","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0140","first-page":"3","article-title":"The early history of automated deduction","volume":"Vol. I","author":"Davis","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0145","series-title":"Proceedings CADE-15: International Conference on Automated Deduction","first-page":"191","article-title":"A resolution decision procedure for the guarded fragment","author":"de Nivelle","year":"1998"},{"year":"1999","series-title":"A new translation method for S4","author":"de Nivelle","key":"10.1016\/B978-044450813-3\/50023-0_bb0150"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0155","unstructured":"de Nivelle H. and de Rijke M. [to appear], \u2018Deciding the guarded fragments by resolution\u2019, Journal of Symbolic Computation."},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0160","article-title":"Extending Modal Logic","author":"de Rijke","year":"1993","journal-title":"PhD thesis, ILLC, University of Amsterdam"},{"year":"1999","series-title":"Restricted description languages","author":"de Rijke","key":"10.1016\/B978-044450813-3\/50023-0_bb0165"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0170","first-page":"609","article-title":"Equality reasoning in sequent-based calculi","volume":"Vol. I","author":"Degtyarev","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0175","first-page":"179","article-title":"The inverse method","volume":"Vol. I","author":"Degtyarev","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0180","series-title":"Proceedings FTP'98: International Workshop on First-Order Theorem Proving","first-page":"127","article-title":"An O((n log n)3)-time transformation from Grz into decidable fragments of classical first-order logic","author":"Demri","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0185","first-page":"533","article-title":"Rewriting","volume":"Vol. I","author":"Dershowitz","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0190","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\/50023-0_sb0190","doi-asserted-by":"crossref","first-page":"406","DOI":"10.1016\/S0022-0000(70)80041-1","article-title":"Tree acceptors and some of their applications","volume":"4","author":"Doner","year":"1970","journal-title":"Journal of Computer and System Sciences"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0200","first-page":"1009","article-title":"Higher-order unification and matching","volume":"Vol. II","author":"Dowek","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0205","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0022-0000(85)90001-7","article-title":"Decision procedures and expressiveness in the temporal logic of brnaching time","volume":"30","author":"Emerson","year":"1985","journal-title":"Journal of Computer and System Sciences"},{"year":"1995","series-title":"Reasoning About Knowledge","author":"Fagin","key":"10.1016\/B978-044450813-3\/50023-0_bb0210"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0215","series-title":"Proceedings CADE'88: International Conference on Automated Deduction","article-title":"Linear modal deductions","author":"Fari\u00f1as del Cerro","year":"1988"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0220","first-page":"1791","article-title":"Resolution decision procedures","volume":"Vol. II","author":"Ferm\u00fcller","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0225","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-56732-1","article-title":"Resolution Methods for the Decision Problem","author":"Ferm\u00fcller","year":"1993"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0230","first-page":"331","article-title":"Propositional quantifiers in modal logic","volume":"36","author":"Fine","year":"1970","journal-title":"Theoria"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0235","first-page":"237","article-title":"Decidability results in non-classical logics","volume":"10","author":"Gabbay","year":"1971","journal-title":"Annals of Mathematical Logic"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0240","doi-asserted-by":"crossref","first-page":"478","DOI":"10.1007\/BF02771736","article-title":"On decidable, finitely axiomatizable modal and tense logics without the finite model property I","volume":"10","author":"Gabbay","year":"1971","journal-title":"Israel Journal of Mathematics"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0245","doi-asserted-by":"crossref","first-page":"496","DOI":"10.1007\/BF02771737","article-title":"On decidable, finitely axiomatizable modal and tense logics without the finite model property II","volume":"10","author":"Gabbay","year":"1971","journal-title":"Israel Journal of Mathematics"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0250","series-title":"Aspects of Philosophical Logic","first-page":"91","article-title":"Expressive functional completeness in tense logic (preliminary report)","author":"Gabbay","year":"1981"},{"volume":"Vol. 2","year":"1984","key":"10.1016\/B978-044450813-3\/50023-0_bb0255"},{"year":"1994","series-title":"Temporal Logic: Mathematical Foundations and Computational Aspects","author":"Gabbay","key":"10.1016\/B978-044450813-3\/50023-0_bb0260"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0265","series-title":"Aspects of Philosophical Logic","first-page":"67","article-title":"An irreflexivity lemma with applications to axiomatizations of conditions on tense frames","author":"Gabbay","year":"1981"},{"volume":"Vol. 126","year":"1996","author":"Gabbay","key":"10.1016\/B978-044450813-3\/50023-0_bb0270"},{"year":"1999","series-title":"Fibring Logics","author":"Gabbay","key":"10.1016\/B978-044450813-3\/50023-0_bb0275"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0280","series-title":"Proceedings LICS'99: Logic in Computer Science","first-page":"295","article-title":"A superposition decision procedure for the guarded fragment with equality","author":"Ganzinger","year":"1999"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0285","series-title":"Proceedings LICS'99: Logic in Computer Science","first-page":"24","article-title":"The two-variable guarded fragment with transitive relations","author":"Ganzinger","year":"1999"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0290","series-title":"Proceedings DEON-94: International Workshop on Deontic Logic in Computer Science","article-title":"Translating non-normal modal logics into normal modal logics","author":"Gasquet","year":"1993"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0295","first-page":"403","article-title":"SAT-based decision procedures for classical modal logics","author":"Giunchiglia","year":"2000"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0300","first-page":"113","article-title":"Ein Spezialfall des Entscheidungsproblem der theoretischen Logik","volume":"2","author":"G\u00f6del","year":"1932","journal-title":"Ergebn. math. Kolloq."},{"year":"1992","series-title":"Logics of Time and Computation","author":"Goldblatt","key":"10.1016\/B978-044450813-3\/50023-0_bb0305"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0310","article-title":"On the restraining power of guards","author":"Gr\u00e4del","year":"2000","journal-title":"Journal of Symbolic Logic"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0315","series-title":"Proceedings LICS'97: Logic in Computer Science","first-page":"306","article-title":"Two-variable logic with counting is decidable","author":"Gr\u00e4del","year":"1997"},{"key":"10.1016\/B978-044450813-3\/50023-0_sb0315","series-title":"Proceedings STACS'97","first-page":"249","article-title":"Undecidability results on two-variable logics","author":"Gr\u00e4del","year":"1997"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0325","series-title":"Proceedings LICS'99: Logic in Computer Science","first-page":"45","article-title":"Guarded fixed point logic","author":"Gr\u00e4del","year":"1999"},{"article-title":"Term Indexing","year":"1996","author":"Graf","key":"10.1016\/B978-044450813-3\/50023-0_bb0330"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0335","first-page":"100","article-title":"Tableaux and related methods","volume":"Vol. I","author":"H\u00e4hnle","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0340","series-title":"Perspectives in Mathematical Logic","article-title":"Metamathematics of First-Order Arithmetic","author":"H\u00e1jek","year":"1991"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0345","doi-asserted-by":"crossref","first-page":"361","DOI":"10.1016\/0004-3702(95)00018-A","article-title":"The effect of bounding the number of primitive propositions and the depth of nesting on the complexity of modal logic","volume":"75","author":"Halpern","year":"1995","journal-title":"Artificial Intelligence"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0350","first-page":"497","article-title":"Dynamic logic","volume":"Vol. 2","author":"Harel","year":"1984"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0355","series-title":"S\u00e9miniare de Math\u00e9matique Sup\u00e9rieures 21","article-title":"Logical systems containing only a finite number of symbols","author":"Henkin","year":"1967"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0360","series-title":"Proceedings TACAS'95","first-page":"479","article-title":"MONA: Monadic second-order logic in practice","author":"Henriksen","year":"1995"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0365","article-title":"Raisonnement Automatique en Logique Modale et Algorithmes d'unification","author":"Herzig","year":"1989","journal-title":"PhD thesis, Universit\u00e9 Paul-Sabatier, Toulouse"},{"year":"1990","series-title":"A translation from propositional modal logic G into K4","author":"Herzig","key":"10.1016\/B978-044450813-3\/50023-0_bb0370"},{"issue":"3","key":"10.1016\/B978-044450813-3\/50023-0_bb0375","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1093\/jigpal\/8.3.293","article-title":"An analysis of emperical testing for modal decision procedures","volume":"8","author":"Horrocks","year":"2000","journal-title":"Logic Journal of the IGPL"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0380","article-title":"Resolution-Based Decision Procedures for Subclasses of First-Order Logic","author":"Hustadt","year":"1999","journal-title":"PhD thesis, Max-Planck Institute for Computer Science, Saarbr\u00fccken"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0385","series-title":"Proceedings Tableaux'98","first-page":"36","article-title":"Optimised functional translation and resolution","author":"Hustadt","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0390","series-title":"Proceedings LICS'87: Logic in Computer Science","first-page":"236","article-title":"Definability with bounded number of bound variables","author":"Immerman","year":"1987"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0395","series-title":"Proceedings CONCUR'96","first-page":"263","article-title":"On the expressive completeness of the propositional \u03bc-calculus w.r.t. monadic second-order logic","author":"Janin","year":"1996"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0400","doi-asserted-by":"crossref","first-page":"398","DOI":"10.1145\/321958.321960","article-title":"Resolution strategies as decision procedures","volume":"23","author":"Joyner","year":"1976","journal-title":"Journal of the ACM"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0405","doi-asserted-by":"crossref","first-page":"466","DOI":"10.1007\/BF01452848","article-title":"\u00dcber die Erf\u00fcllbarkeit derjenigen Z\u00e1hlausdr\u00fccke, welche in der Normalform zwei benachbarte Allzeichen enthalten","volume":"108","author":"Kalm\u00e1r","year":"1933","journal-title":"Math. Annal."},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0410","doi-asserted-by":"crossref","first-page":"99","DOI":"10.2307\/2586754","article-title":"Normal monomodal logics can simulate all others","volume":"64","author":"Kracht","year":"1999","journal-title":"Journal of Symbolic Logic"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0415","doi-asserted-by":"crossref","first-page":"403","DOI":"10.1023\/A:1008223921944","article-title":"Bisimulations for temporal logic","volume":"6","author":"Kurtonina","year":"1997","journal-title":"Journal of Logic, Language and Information"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0420","doi-asserted-by":"crossref","first-page":"303","DOI":"10.1016\/S0004-3702(98)00109-X","article-title":"Expressiveness of concept expressions in first-order description logics","volume":"107","author":"Kurtonina","year":"1999","journal-title":"Artificial Intelligence"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0425","doi-asserted-by":"crossref","first-page":"467","DOI":"10.1137\/0206033","article-title":"The computational complexity of provability in systems of modal logic","volume":"6","author":"Ladner","year":"1977","journal-title":"SIAM Journal on Computing"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0430","first-page":"2015","article-title":"Model elimination and connection tableau procedures","volume":"Vol. II","author":"Letz","year":"2001"},{"article-title":"Selected Works","year":"1970","author":"Lukasiewicz","key":"10.1016\/B978-044450813-3\/50023-0_bb0435"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0440","series-title":"Proceedings CADE-11","first-page":"209","article-title":"Experiments in automated deduction with condensed detachment","author":"McCune","year":"1992"},{"key":"10.1016\/B978-044450813-3\/50023-0_sb0440","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1090\/trans2\/143\/01","article-title":"Resolution calculi for modal logics","volume":"143","author":"Mints","year":"1989","journal-title":"Amer. Math. Soc. Transl."},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0450","series-title":"Proceedings LICS'99: Logic in Computer Science","first-page":"360","article-title":"On the expressive power of CTL","author":"Moller","year":"1999"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0455","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1002\/malq.19750210118","article-title":"On languages with two variables","volume":"21","author":"Mortimer","year":"1975","journal-title":"Zeitschr. f. math. Logik u. Grundlagen d. Math."},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0460","first-page":"371","article-title":"Paramodulation-based theorem proving","volume":"Vol. I","author":"Nieuwenhuis","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0465","article-title":"First-order modal logic theorem proving and standard PROLOG","author":"Nonnengart","year":"1992","journal-title":"Technical Report MPI-I-92-228, Max-Planck-Institute for Computer Science, Saarbr\u00fccken, Germany"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0470","series-title":"Proceedings IJCAI-13","first-page":"80","article-title":"First-order modal logic theorem proving and functional simulation","author":"Nonnengart","year":"1993"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0475","article-title":"A Resolution-Based Calculus for Temporal Logics","author":"Nonnengart","year":"1995","journal-title":"PhD thesis, Universit\u00e4t des Saarlandes, Saarbr\u00fccken, Germany"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0480","series-title":"Proceedings CADE-13: International Conference on Automated Deduction","first-page":"598","article-title":"Resolution-based calculi for modal and temporal logics","author":"Nonnengart","year":"1996"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0485","first-page":"335","article-title":"Computing small clause normal forms","volume":"Vol. I","author":"Nonnengart","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0490","series-title":"Proceedings CADE-88: International Conference on Automated Deduction","first-page":"500","article-title":"A resolution calculus for modal logics","author":"Ohlbach","year":"1988"},{"key":"10.1016\/B978-044450813-3\/50023-0_sb0490","article-title":"A resolution calculus for modal logics, SEKI Report SR-88-08, FB Informatik, Universit\u00e4t Kaiserslautern, Germany","author":"Ohlbach","year":"1988","journal-title":"PhD Thesis"},{"key":"10.1016\/B978-044450813-3\/50023-0_sb0495","series-title":"Proceedings CADE-88: International Conference on Automated Deduction","first-page":"500","article-title":"A resolution calculus for modal logics","author":"Ohlbach","year":"1988"},{"issue":"5","key":"10.1016\/B978-044450813-3\/50023-0_bb0500","doi-asserted-by":"crossref","first-page":"691","DOI":"10.1093\/logcom\/1.5.691","article-title":"Semantics based translation methods for modal logics","volume":"1","author":"Ohlbach","year":"1991","journal-title":"Journal of Logic and Computation"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0505","series-title":"Proceedings CADE-15: International Conference on Automated Deduction","first-page":"205","article-title":"Combining Hilbert-style and semantic reasoning in a resolution framework","author":"Ohlbach","year":"1998"},{"issue":"3","key":"10.1016\/B978-044450813-3\/50023-0_bb0510","doi-asserted-by":"crossref","first-page":"317","DOI":"10.1023\/A:1005894718064","article-title":"Elimination of self-resolving clauses","volume":"20","author":"Ohlbach","year":"1998","journal-title":"Journal of Automated Reasoning"},{"issue":"5","key":"10.1016\/B978-044450813-3\/50023-0_bb0515","doi-asserted-by":"crossref","first-page":"581","DOI":"10.1093\/logcom\/7.5.581","article-title":"Functional translation and second-order frame properties of modal logics","volume":"7","author":"Ohlbach","year":"1997","journal-title":"Journal of Logic and Computation"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0520","series-title":"Proceedings CADE-7: International Conference on Automated Deduction","first-page":"496","article-title":"Solving a problem in relevance logic with an automated theorem prover","author":"Ohlbach","year":"1984"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0525","first-page":"1403","article-title":"Encoding two-valued nonclassical logics in classical logic","volume":"Vol. II","author":"Ohlbach","year":"2001"},{"article-title":"Bounded Variable Logics and Counting \u2013 A Study in Finite Models","year":"1997","author":"Otto","key":"10.1016\/B978-044450813-3\/50023-0_bb0530"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0535","series-title":"Proceedings DL'98","first-page":"87","article-title":"DLP system description","author":"Patel-Schneider","year":"1998"},{"article-title":"Isabelle: a Generic Theorem Prover","year":"1994","author":"Paulson","key":"10.1016\/B978-044450813-3\/50023-0_bb0540"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0545","first-page":"1063","article-title":"Logical frameworks","volume":"Vol. II","author":"Pfenning","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0550","article-title":"T-theorem proving I","author":"Policriti","year":"1992","journal-title":"Research report 08\/92, Universit\u00e0 di Udine"},{"year":"1953","series-title":"From a Logical Point of View","author":"Quine","key":"10.1016\/B978-044450813-3\/50023-0_sb0555"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0560","first-page":"1","article-title":"Decidability of second-order theories and automata on infinite trees","volume":"141","author":"Rabin","year":"1969","journal-title":"Transactions of the American Mathematical Society"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0565","first-page":"1853","article-title":"Term indexing","volume":"Vol. II","author":"Ramakrishnan","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0570","doi-asserted-by":"crossref","first-page":"427","DOI":"10.1023\/A:1008275906015","article-title":"Modal logic over finite structures","volume":"6","author":"Rosen","year":"1997","journal-title":"Journal of Logic, Language and Information"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0575","doi-asserted-by":"crossref","unstructured":"Rounds W. [1997], Feature logics, in van Benthem and ter Meulen [1997].","DOI":"10.1016\/B978-044481714-3\/50012-6"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0580","series-title":"Proceedings of the 3rd Scandinavian Logic Symposium","first-page":"110","article-title":"Completeness and correspondence in the first and second order semantics for modal logics","author":"Sahlqvist","year":"1975"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0585","article-title":"Optimised Modal Translation and Resolution","author":"Schmidt","year":"1997","journal-title":"PhD thesis, Universit\u00e4t des Saarlandes"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0590","series-title":"Proceedings RTA'98: Term Rewriting and Applications","first-page":"106","article-title":"E-unification for subsystems of S4","author":"Schmidt","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0595","series-title":"Advances in Modal Logic","first-page":"189","article-title":"Resolution is a decision procedure for many propositional modal logics","author":"Schmidt","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0600","doi-asserted-by":"crossref","first-page":"572","DOI":"10.1007\/BF01449155","article-title":"Untersuchungen zum Entscheidungsproblem der mathematischen Logik","volume":"109","author":"Sch\u00fctte","year":"1934","journal-title":"Math. Annal."},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0605","first-page":"377","article-title":"A decision method for validity of sentences in two variables","volume":"27","author":"Scott","year":"1962","journal-title":"Journal of Symbolic Logic"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0610","article-title":"An essay in classical modal logic","volume":"Volume 1\u20133","author":"Segerberg","year":"1971","journal-title":"Technical Report 13, University of Uppsala, Filosofiska Studier"},{"year":"2000","series-title":"TANCS: Tableaux Non Classical Systems Comparison","author":"TAN","key":"10.1016\/B978-044450813-3\/50023-0_bb0615"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0620","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1007\/BF01691346","article-title":"Generalized finite automata theory with an application to a decision problem of second-order logic","volume":"2","author":"Thatcher","year":"1968","journal-title":"Mathematical Systems Theory"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0625","doi-asserted-by":"crossref","first-page":"549","DOI":"10.2307\/2272895","article-title":"Reduction of tense logic to modal logic I","volume":"39","author":"Thomason","year":"1974","journal-title":"Journal of Symbolic Logic"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0630","doi-asserted-by":"crossref","first-page":"154","DOI":"10.1111\/j.1755-2567.1975.tb00555.x","article-title":"Reduction of tense logic to modal logic II","volume":"41","author":"Thomason","year":"1975","journal-title":"Theoria"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0635","article-title":"Modal Correspondence Theory","author":"van Benthem","year":"1976","journal-title":"PhD thesis, Mathematisch Instituut & Instituut voor Grondslagenonderzoek, University of Amsterdam"},{"year":"1983","series-title":"Modal Logic and Classical Logic","author":"van Benthem","key":"10.1016\/B978-044450813-3\/50023-0_bb0640"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0645","series-title":"Extensions of Classical Logic, Synthese Library","first-page":"167","article-title":"Correspondence theory","volume":"Vol. II","author":"van Benthem","year":"1984"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0650","article-title":"Dynamic bits and pieces","author":"van Benthem","year":"1997","journal-title":"Technical Report LP-1997-01, ILLC, University of Amsterdam"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0655","doi-asserted-by":"crossref","first-page":"251","DOI":"10.1093\/logcom\/7.2.251","article-title":"Modal deduction in second-order logic and set theory I","volume":"7","author":"van Benthem","year":"1997","journal-title":"Journal of Logic and Computation"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0660","doi-asserted-by":"crossref","first-page":"387","DOI":"10.1023\/A:1005037512998","article-title":"Modal deduction in second-order logic and set theory II","volume":"60","author":"van Benthem","year":"1998","journal-title":"Studia Logica"},{"year":"1997","series-title":"Handbook of Logic and Language","key":"10.1016\/B978-044450813-3\/50023-0_bb0665"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0670","series-title":"DIMACS Series in Discrete Mathematics and Theoretical Computer Science 31","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1090\/dimacs\/031\/05","article-title":"Why is modal logic so robustly decidable?","author":"Vardi","year":"1997"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0675","first-page":"1487","article-title":"Connections in nonclassical logics","volume":"Vol. II","author":"Waaler","year":"2001"},{"year":"1987","series-title":"A Many-Sorted Calculus Based on Resolution and Paramodulation","author":"Walther","key":"10.1016\/B978-044450813-3\/50023-0_bb0680"},{"key":"10.1016\/B978-044450813-3\/50023-0_sb0680","first-page":"1965","article-title":"Combining superposition, sorts and splitting","volume":"Vol. II","author":"Weidenbach","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50023-0_bb0690","first-page":"22","article-title":"Modal resolutions","volume":"33","author":"Zamov","year":"1989","journal-title":"Soviet Math."}],"container-title":["Handbook of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:B9780444508133500230?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:B9780444508133500230?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T20:55:17Z","timestamp":1556484917000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/B9780444508133500230"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9780444508133"],"references-count":138,"URL":"https:\/\/doi.org\/10.1016\/b978-044450813-3\/50023-0","relation":{},"subject":[],"published":{"date-parts":[[2001]]}}}