{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T23:18:50Z","timestamp":1761607130820,"version":"build-2065373602"},"reference-count":200,"publisher":"Elsevier","isbn-type":[{"type":"print","value":"9780444516909"}],"license":[{"start":{"date-parts":[[2007,1,1]],"date-time":"2007-01-01T00:00:00Z","timestamp":1167609600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2007,1,1]],"date-time":"2007-01-01T00:00:00Z","timestamp":1167609600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2007]]},"DOI":"10.1016\/s1570-2464(07)80007-3","type":"book-chapter","created":{"date-parts":[[2007,10,4]],"date-time":"2007-10-04T09:38:50Z","timestamp":1191490730000},"page":"181-245","source":"Crossref","is-referenced-by-count":27,"title":["4 Computational modal logic"],"prefix":"10.1016","member":"78","reference":[{"key":"10.1016\/S1570-2464(07)80007-3_bib1","series-title":"Proceedings of the 8th International Conference on Automated Deduction (CADES), volume 230 of Lecture Notes in Computer Science","first-page":"172","article-title":"Modal theorem proving","author":"Abadi","year":"1986"},{"key":"10.1016\/S1570-2464(07)80007-3_bib2","series-title":"Proceedings of the International Conference on Fifth Generation Computer Systems '92","first-page":"833","article-title":"Implementing Prolog extensions: a parallel inference machine","author":"Alliot","year":"1986"},{"issue":"3","key":"10.1016\/S1570-2464(07)80007-3_bib3","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\/S1570-2464(07)80007-3_bib4","series-title":"PhD thesis","article-title":"Logic Engineering. The Case of Description and Hybrid Logics","author":"Areces","year":"2000"},{"key":"10.1016\/S1570-2464(07)80007-3_bib5","series-title":"Annual Conference of the European Association for Computer Science Logic (CSL '99), volume 1683 of Lecture Notes in Computer Science","first-page":"307","article-title":"A road-map on complexity for hybrid logics","author":"Areces","year":"1999"},{"key":"10.1016\/S1570-2464(07)80007-3_bib6","series-title":"Proceedings of the 16th International Conference on Automated Deduction (CADE- 16), volume 1632 of Lecture Notes in Artificial Intelligence","first-page":"187","article-title":"Prefixed resolution: A resolution method for modal and description logics","author":"Areces","year":"1999"},{"issue":"5","key":"10.1016\/S1570-2464(07)80007-3_bib7","doi-asserted-by":"crossref","first-page":"717","DOI":"10.1093\/logcom\/11.5.717","article-title":"Resolution in modal, description and hybrid logic","volume":"ll","author":"Areces","year":"2001","journal-title":"Journal of Logic and Computation"},{"key":"10.1016\/S1570-2464(07)80007-3_bib8","unstructured":"C. Areces, R. Gennari, J. Heguiabehere, and M. de Rijke. A simple ordering for deciding modal logic. Forthcoming."},{"key":"10.1016\/S1570-2464(07)80007-3_bib9","series-title":"Proceedings of the 14th European Conference on Artificial Intelligence (ECAI 2000)","first-page":"199","article-title":"Tree-based heuristic in modal theorem proving","author":"Areces","year":"2000"},{"key":"10.1016\/S1570-2464(07)80007-3_bib10","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"},{"article-title":"Augmenting concept languages by transitive closure of roles: An alternative to terminological cycles","year":"1990","author":"Baader","key":"10.1016\/S1570-2464(07)80007-3_bib11"},{"issue":"2\u20134","key":"10.1016\/S1570-2464(07)80007-3_bib12","first-page":"247","article-title":"From tableaux to automata for description logics","volume":"57","author":"Baader","year":"2003","journal-title":"Fundamenta Infor- maticae"},{"key":"10.1016\/S1570-2464(07)80007-3_bib13","series-title":"Proceed- ings of the International Joint Conference on Automated Reasoning (IJCAR-01), volume 2083 of Lecture Notes in Artificial Intelligence","first-page":"92","article-title":"The inverse method implements the automata approach for modal satisfiability","author":"Baader","year":"2001"},{"issue":"3","key":"10.1016\/S1570-2464(07)80007-3_bib14","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1093\/logcom\/4.3.217","article-title":"Rewrite-based equational theorem proving with selection and simplification","volume":"4","author":"Bachmair","year":"1994","journal-title":"Journal of Logic and Computation"},{"issue":"6","key":"10.1016\/S1570-2464(07)80007-3_bib15","doi-asserted-by":"crossref","first-page":"1007","DOI":"10.1145\/293347.293352","article-title":"Ordered chaining calculi for first-order theories of transitive relations","volume":"45","author":"Bachmair","year":"1998","journal-title":"Journal of the ACM"},{"key":"10.1016\/S1570-2464(07)80007-3_bib16","first-page":"19","article-title":"Resolution theorem proving","volume":"volume I","author":"Bachmair","year":"2001"},{"issue":"2","key":"10.1016\/S1570-2464(07)80007-3_bib17","doi-asserted-by":"crossref","first-page":"172","DOI":"10.1006\/inco.1995.1131","article-title":"Basic paramodulation","volume":"121","author":"Bachmair","year":"1995","journal-title":"Information and Computation"},{"key":"10.1016\/S1570-2464(07)80007-3_bib18","series-title":"Proceedings of the Third Kurt G\u00f6del Colloquium (KGC '93), volume 713 of Lecture Notes in Computer Science","first-page":"83","article-title":"Superposition with simplification as a decision procedure for the monadic class with equality","author":"Bachmair","year":"1993"},{"key":"10.1016\/S1570-2464(07)80007-3_bib19","series-title":"PhD thesis","article-title":"Intelligent Backtracking on Constraint Satisfaction Problems: Experimental and Theoretical Results","author":"Baker","year":"1995"},{"key":"10.1016\/S1570-2464(07)80007-3_bib20","series-title":"Proceedings of the 1988 International Conference on Fifth Generation Computer Systems","first-page":"507","article-title":"Declarative semantics for modal logic programs","author":"Balbiani","year":"1988"},{"key":"10.1016\/S1570-2464(07)80007-3_bib21","series-title":"Proceedings of the International Workshop on Processing Declar- ative Knowledge (PDK '91), volume 567 of Lecture Notes in Artificial Intelligence","first-page":"366","article-title":"TIM: The Toulouse Inference Machine for non-classical logic pro- gramming","author":"Balbiani","year":"1991"},{"key":"10.1016\/S1570-2464(07)80007-3_bib22","series-title":"PhD thesis","article-title":"Normal Multimodal Logics: Automatic Deduction and Logic Programming Extension","author":"Baldoni","year":"1998"},{"key":"10.1016\/S1570-2464(07)80007-3_bib23","series-title":"Joint International Conference and Symposium on Logic Programming","first-page":"52","article-title":"A framework for a modal logic programming","author":"Baldoni","year":"1996"},{"issue":"2\u20134","key":"10.1016\/S1570-2464(07)80007-3_bib24","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1023\/B:AMAI.0000031196.24935.b5","article-title":"Programming rational agents in a modal action logic","volume":"41","author":"Baldoni","year":"2004","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"10.1016\/S1570-2464(07)80007-3_bib25","series-title":"Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX '98), volume 1397 of Lecture Notes inIntelligence","first-page":"35","article-title":"Logics Workbench 1.0","author":"Balsiger","year":"1998"},{"key":"10.1016\/S1570-2464(07)80007-3_bib26","series-title":"Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX '99), volume 1617 of Lecture Notes inIntelligence","first-page":"51","article-title":"Merge path improvements for minimal model hyper tableaux","author":"Baumgartner","year":"1999"},{"key":"10.1016\/S1570-2464(07)80007-3_bib27","series-title":"Proceedings of the Third International Joint Conference on Automated Reasoning (IJCAR 2006)","article-title":"Improved bottom-up model generation","author":"Baumgartner","year":"2006"},{"key":"10.1016\/S1570-2464(07)80007-3_bib28","series-title":"Proceedings of the 2nd International Workshop on Computer Aided Verification (CAV '90), volume 531 of Lecture Notes in Computer Science","first-page":"197","article-title":"Minimal model generation","author":"Bouajjani","year":"1991"},{"key":"10.1016\/S1570-2464(07)80007-3_bib29","doi-asserted-by":"crossref","first-page":"283","DOI":"10.1016\/0747-7171(92)90009-S","article-title":"An optimality result for clause form translation","volume":"14","author":"Boy de la Tour","year":"1992","journal-title":"Journal of Symbolic Computation"},{"issue":"5","key":"10.1016\/S1570-2464(07)80007-3_bib30","doi-asserted-by":"crossref","first-page":"629","DOI":"10.1093\/jigpal\/8.5.629","article-title":"A cut-free Gentzen formulation of the modal logic S5","volume":"8","author":"Bra\u00fcner","year":"2000","journal-title":"Logic Journal of the IGPL"},{"issue":"1","key":"10.1016\/S1570-2464(07)80007-3_bib31","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1023\/A:1006291616338","article-title":"Positive unit hyperresolution tableaux for minimal model generation","volume":"25","author":"Bry","year":"2000","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/S1570-2464(07)80007-3_bib32","series-title":"Proceedings of the 6th International Conference on Principles of Knowledge Representation and Reasoning (KR '98)","first-page":"2","article-title":"Description logic framework for information integration","author":"Calvanese","year":"1998"},{"key":"10.1016\/S1570-2464(07)80007-3_bib33","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1016\/0304-3975(91)90181-Z","article-title":"Resolution for some first order modal systems","volume":"85","author":"Cialdea","year":"1991","journal-title":"Theoretical Computer Science"},{"year":"1999","series-title":"Model Checking","author":"Clarke","key":"10.1016\/S1570-2464(07)80007-3_bib34"},{"key":"10.1016\/S1570-2464(07)80007-3_bib35","first-page":"1635","article-title":"Model checking","volume":"volume II","author":"Clarke","year":"2001"},{"key":"10.1016\/S1570-2464(07)80007-3_bib36","first-page":"17","article-title":"Elementary canonical formulae: a survey on syntactic, algorithmic, and model-theoretic aspects","volume":"Volume 5","author":"Conradie","year":"2005"},{"issue":"1\u20135","key":"10.1016\/S1570-2464(07)80007-3_bib37","first-page":"1","article-title":"Algorithmic correspondence and completeness in modal logic. i. the core algorithm SQEMA","volume":"2","author":"Conradie","year":"2006","journal-title":"Logical Methods in Computer Science"},{"issue":"1","key":"10.1016\/S1570-2464(07)80007-3_bib38","doi-asserted-by":"crossref","first-page":"36","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"},{"key":"10.1016\/S1570-2464(07)80007-3_bib39","doi-asserted-by":"crossref","first-page":"249","DOI":"10.2307\/2266613","article-title":"The elimination theorem when modality is present","volume":"17","author":"Curry","year":"1952","journal-title":"Journal of Symbolic Logic"},{"key":"10.1016\/S1570-2464(07)80007-3_bib40","first-page":"36","article-title":"Are tableaux an improvement on truth-tables?","volume":"1","author":"D'Agostino","year":"1979","journal-title":"Journal of Logic, Language, and Information"},{"key":"10.1016\/S1570-2464(07)80007-3_bib41","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"},{"key":"10.1016\/S1570-2464(07)80007-3_bib42","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":"Journal of the ACM"},{"issue":"2","key":"10.1016\/S1570-2464(07)80007-3_bib43","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1007\/BF00173700","article-title":"Eliminating 'converse' from converse PDL","volume":"5","author":"De Giacomo","year":"1962","journal-title":"Journal of Logic, Language and Information"},{"key":"10.1016\/S1570-2464(07)80007-3_bib44","series-title":"Proceedings of the 12th National Conference on Artificial Intelligence (AAAI-94)","first-page":"205","article-title":"Boosting the correspondence between description logics and propositional dy- namic logics (extended abstract)","author":"De Giacomo","year":"1994"},{"issue":"1\u20132","key":"10.1016\/S1570-2464(07)80007-3_bib45","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1006\/inco.1999.2852","article-title":"Combining deduction and model checking into tableaux and algorithms for converse-pdl","volume":"160","author":"De Giacomo","year":"2000","journal-title":"Information and Computation"},{"key":"10.1016\/S1570-2464(07)80007-3_bib46","series-title":"PhD thesis","article-title":"Ordering refinements of resolution","author":"De Nivelle","year":"1996"},{"key":"10.1016\/S1570-2464(07)80007-3_bib47","series-title":"Proceedings of the 8th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2001), volume 2250 of Lecture Notes in Artificial Intelligence","first-page":"172","article-title":"Splitting through new proposition symbols","author":"De Nivelle","year":"2001"},{"issue":"1","key":"10.1016\/S1570-2464(07)80007-3_bib48","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1016\/S0747-7171(02)00092-5","article-title":"Deciding the guarded fragment by resolution","volume":"35","author":"De Nivelle","year":"2003","journal-title":"Journal of Symbolic Computation"},{"issue":"3","key":"10.1016\/S1570-2464(07)80007-3_bib49","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"},{"issue":"1","key":"10.1016\/S1570-2464(07)80007-3_bib50","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1016\/0304-3975(92)90290-V","article-title":"Multimodal logic programming using equational and order-sorted logic","volume":"105","author":"Debart","year":"1992","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1570-2464(07)80007-3_bib51","first-page":"179","article-title":"The inverse method","volume":"volume I","author":"Degtyarev","year":"2001"},{"key":"10.1016\/S1570-2464(07)80007-3_bib52","first-page":"533","article-title":"Rewriting","volume":"volume I","author":"Dershowitz","year":"2001"},{"issue":"1","key":"10.1016\/S1570-2464(07)80007-3_bib53","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1016\/S0004-3702(01)00052-2","article-title":"Temporal Agent Reasoning","volume":"127","author":"Dix","year":"2001","journal-title":"Artificial Intelligence"},{"issue":"3","key":"10.1016\/S1570-2464(07)80007-3_bib54","doi-asserted-by":"crossref","first-page":"345","DOI":"10.1093\/logcom\/8.3.345","article-title":"Resolution for temporal logics of knowledge","volume":"8","author":"Dixon","year":"1998","journal-title":"Journal of Logic and Computaton"},{"issue":"3","key":"10.1016\/S1570-2464(07)80007-3_bib55","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1023\/A:1005722130532","article-title":"Computing circumscription revisited: A reduction algorithm","volume":"18","author":"Doherty","year":"1997","journal-title":"Journal of Automated Reasoning"},{"issue":"1","key":"10.1016\/S1570-2464(07)80007-3_bib56","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1016\/S0004-3702(00)00070-9","article-title":"Exptime tableaux for ACC","volume":"124","author":"Donini","year":"2000","journal-title":"Artificial Intelligence"},{"issue":"1-3","key":"10.1016\/S1570-2464(07)80007-3_bib57","doi-asserted-by":"crossref","first-page":"221","DOI":"10.1016\/S0304-3975(03)00361-X","article-title":"An efficient algorithm for computing bisimulation equivalence","volume":"311","author":"Dovier","year":"2004","journal-title":"Theoretical Computer Science"},{"year":"1996","series-title":"Quantifier elimination in second-order predicate logic","author":"Engel","key":"10.1016\/S1570-2464(07)80007-3_bib58"},{"issue":"1","key":"10.1016\/S1570-2464(07)80007-3_bib59","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(89)90137-0","article-title":"Modal resolution in clausal form","volume":"65","author":"Enjalbert","year":"1989","journal-title":"Theoretical Computer Science"},{"year":"1996","series-title":"Reasoning About Knowledge","author":"Fagin","key":"10.1016\/S1570-2464(07)80007-3_bib60"},{"issue":"2","key":"10.1016\/S1570-2464(07)80007-3_bib61","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1016\/0020-0190(82)90085-0","article-title":"A simple deduction method for modal logic","volume":"14","author":"Fari\u00f1as del Cerro","year":"1982","journal-title":"Information Processing Letters"},{"key":"10.1016\/S1570-2464(07)80007-3_bib62","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1007\/BF03037381","article-title":"MOLOG: A system that extends PROLOG with modal logic","volume":"4","author":"Fari\u00f1as del Cerro","year":"1986","journal-title":"New Generation Computing"},{"key":"10.1016\/S1570-2464(07)80007-3_bib63","unstructured":"L. Fari\u00f1as del Cerro and A. Herzig. MOLOG. http: \/\/www. irit .f r\/ACTIVITES\/EQ_ALG\/Herzig\/ molog.html."},{"key":"10.1016\/S1570-2464(07)80007-3_bib64","first-page":"499","article-title":"Modal deduction with applications in epistemic and temporal logics","volume":"volume 4","author":"Fari\u00f1as del Cerro","year":"1995"},{"key":"10.1016\/S1570-2464(07)80007-3_bib65","first-page":"1791","article-title":"Resolution decision procedures","volume":"volume II","author":"Ferm\u00fcller","year":"2001"},{"key":"10.1016\/S1570-2464(07)80007-3_bib66","series-title":"In Proceedings of the Third International Conference on Formal Description Techniques (FORTE '90)","first-page":"95","article-title":"Verification bisimulations \u2018on the fly\u2019","author":"Fernandez","year":"1990"},{"issue":"2\u20133","key":"10.1016\/S1570-2464(07)80007-3_bib67","doi-asserted-by":"crossref","first-page":"219","DOI":"10.1016\/0167-6423(90)90071-K","article-title":"An implementation of an efficient algorithm for bisimulation equivalence","volume":"13","author":"Fernandez","year":"1990","journal-title":"Science of Computer Programming"},{"key":"10.1016\/S1570-2464(07)80007-3_bib68","doi-asserted-by":"crossref","first-page":"194","DOI":"10.1016\/0022-0000(79)90046-1","article-title":"Propositional dynamic logic of regular programs","volume":"18","author":"Fischer","year":"1979","journal-title":"Journal of Computer and System Science"},{"key":"10.1016\/S1570-2464(07)80007-3_bib69","series-title":"Revised Papers of the Second International Workshop on Formal Ap- proaches to Agent-Based Systems (FAABS 2002), volume 2699 of Lecture Notes in Artificial Int","first-page":"15","article-title":"Organising logic-based agents","author":"Fisher","year":"2003"},{"key":"10.1016\/S1570-2464(07)80007-3_bib70","series-title":"Proceedings of the IJCAI-93 Workshop on Executable Modal and Temporal Logics, volume 897 of Lecture Notes in Artificial Intelligence","first-page":"15","article-title":"An introduction to executable modal and temporal logics","author":"Fisher","year":"2003"},{"key":"10.1016\/S1570-2464(07)80007-3_bib71","series-title":"Proceedings of the 10th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME '99), volume 1703 of Lec in Computer Science","first-page":"338","article-title":"Bisimulation and model checking","author":"Fisler","year":"1999"},{"issue":"1","key":"10.1016\/S1570-2464(07)80007-3_bib72","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1093\/logcom\/1.1.83","article-title":"Destructive modal resolution","volume":"l","author":"Fitting","year":"1990","journal-title":"Journal of Logic and Computation"},{"key":"10.1016\/S1570-2464(07)80007-3_bib73","series-title":"Working Notes of the ECAI2000 Workshop on Knowledge Representation Meets Databases (KRDB2000)","first-page":"45","article-title":"The i.com tool for intelligent conceptual modelling","author":"Franconi","year":"2000"},{"key":"10.1016\/S1570-2464(07)80007-3_bib74","series-title":"PhD thesis","article-title":"Improvements to Propositional Satisfiability Search Algorithms","author":"Freeman","year":"1995"},{"key":"10.1016\/S1570-2464(07)80007-3_bib75_1","first-page":"35","article-title":"Quantifier elimination in second-order predicate logic","volume":"7","author":"Gabbay","year":"1992","journal-title":"South African Computer Journal"},{"first-page":"425","year":"1992","series-title":"Proceedings of the Third Inter- national Conference on Principles of Knowledge Representation and Reasoning (KR '92)","key":"10.1016\/S1570-2464(07)80007-3_bib75_2"},{"key":"10.1016\/S1570-2464(07)80007-3_bib76","series-title":"Proceedings of the Fourteenth Annual IEEE Symposium on Logic in Computer Science (LICS '99)","first-page":"295","article-title":"A superposition decision procedure for the guarded fragment with equality","author":"Ganzinger","year":"1999"},{"key":"10.1016\/S1570-2464(07)80007-3_bib77","series-title":"Advances in Modal Logic, Volume 2, volume 119 of Lecture Notes","first-page":"225","article-title":"A resolution-based decision procedure for extensions of K4","author":"Ganzinger","year":"2001"},{"article-title":"Performance measurement and analysis of certain search algorithms","year":"1979","author":"Gaschnig","key":"10.1016\/S1570-2464(07)80007-3_bib78"},{"key":"10.1016\/S1570-2464(07)80007-3_bib79","series-title":"Proceedings of the 1st Conference on Theoretical Aspects of Reasoning about Knowledge","first-page":"309","article-title":"A resolution method for quantified modal logics of knowledge and belief","author":"Geissler","year":"1986"},{"key":"10.1016\/S1570-2464(07)80007-3_bib80_1","doi-asserted-by":"crossref","first-page":"176","DOI":"10.1007\/BF01201353","article-title":"Untersuchungen \u00fcber das logische Schlie\u00dfen","volume":"39","author":"Gentzen","year":"1935","journal-title":"Mathematische Zeitschrift"},{"key":"10.1016\/S1570-2464(07)80007-3_bib80_2","doi-asserted-by":"crossref","first-page":"405","DOI":"10.1007\/BF01201363","article-title":"Untersuchungen \u00fcber das logische Schlie\u00dfen","volume":"39","author":"Gentzen","year":"1935","journal-title":"Mathematische Zeitschrift"},{"first-page":"68","year":"1969","series-title":"The Collected Papers of Gerhard Gentzen","key":"10.1016\/S1570-2464(07)80007-3_bib80_3"},{"key":"10.1016\/S1570-2464(07)80007-3_bib81","series-title":"Proceedings of the 8th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2001), volume 2250 of Lecture Notes inIntelligence","first-page":"85","article-title":"Computational space efficiency and minimal model generation for guarded formulae","author":"Georgieva","year":"2001"},{"key":"10.1016\/S1570-2464(07)80007-3_bib82","series-title":"Proceedings of the 18th International Conference on Automated Deduction (CADE-18), volume 2392 of Lecture Notes in Artificial Intelligence","first-page":"260","article-title":"A new clausal class decidable by hyperresolution","author":"Georgieva","year":"2002"},{"issue":"1\u20132","key":"10.1016\/S1570-2464(07)80007-3_bib83","doi-asserted-by":"crossref","first-page":"163","DOI":"10.1016\/S0747-7171(03)00034-8","article-title":"Hyperresolution for guarded formulae","volume":"36","author":"Georgieva","year":"2003","journal-title":"Journal of Symbolic Computa- tion"},{"key":"10.1016\/S1570-2464(07)80007-3_bib84","series-title":"Encyclopedia of Microcomputers","first-page":"393","article-title":"Temporal and modal logic programming languages","author":"Gergatsoulis","year":"2001"},{"issue":"2","key":"10.1016\/S1570-2464(07)80007-3_bib85","doi-asserted-by":"crossref","first-page":"145","DOI":"10.1080\/11663081.2000.10510994","article-title":"Sat vs. translation based decision procedures for modal logics: A comparative evaluation","volume":"10","author":"Giunchiglia","year":"2000","journal-title":"Journal of Applied Non-Classical Logics"},{"key":"10.1016\/S1570-2464(07)80007-3_bib86","series-title":"Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Re- lated Methods (TABLEAUX 2000), volume 1847 of Lecture NotesArtificial Intelligence","first-page":"237","article-title":"A subset-matching size-bounded cache for satisfiability in modal logics","author":"Giunchiglia","year":"2000"},{"key":"10.1016\/S1570-2464(07)80007-3_bib87","series-title":"Proceedings of the 13th Conference on Automated Deduction (CADE-13), volume 1104 of Lecture Notes in Artificial Intelligence","first-page":"583","article-title":"Building decision procedures for modal logics from propositional decision procedures \u2014 the case study of modal K","author":"Giunchiglia","year":"1996"},{"key":"10.1016\/S1570-2464(07)80007-3_bib88","series-title":"Revised Selected Papers of the 7th International Seminar on Relational Meth- ods in Computer Science and the 2nd International Workshop on Kleene Algebra, vol of Lecture Notes in Computer Science","first-page":"149","article-title":"SCAN is complete for all Sahlqvist formulae","author":"Goranko","year":"2004"},{"key":"10.1016\/S1570-2464(07)80007-3_bib89","series-title":"Handbook of Tableau Methods","first-page":"297","article-title":"Tableau methods for modal and temporal logics","author":"Gor\u00e9","year":"1999"},{"key":"10.1016\/S1570-2464(07)80007-3_bib90","series-title":"Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2000), volume 1847 of Lecture Notes in Intelligence","first-page":"1","article-title":"Consistency testing: The RACE experience","author":"Haarslev","year":"2000"},{"key":"10.1016\/S1570-2464(07)80007-3_bib91","series-title":"Proceedings of the 17th International Joint Conference on Artificial Intelligence (IJCAI 2001)","first-page":"161","article-title":"High performance reasoning with very large knowledge bases: A practical case study","author":"Haarslev","year":"2001"},{"key":"10.1016\/S1570-2464(07)80007-3_bib92","series-title":"Handbook of Automated Reasoning","first-page":"101","article-title":"Tableaux and related methods","author":"H\u00e4hnle","year":"2001"},{"key":"10.1016\/S1570-2464(07)80007-3_bib93","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1016\/0004-3702(92)90049-4","article-title":"A guide to completeness and complexity for modal logic of knowledge and belief","volume":"54","author":"Halpern","year":"1992","journal-title":"Artificial Intelligence"},{"key":"10.1016\/S1570-2464(07)80007-3_bib94","series-title":"Proceedings of the 17th International Conference on Automated Deduction (CADE-17), vol- ume 1831 of Lecture Notes in Artificial Intelligence","first-page":"184","article-title":"Efficient minimal model generation using branching lemmas","author":"Hasegawa","year":"2000"},{"key":"10.1016\/S1570-2464(07)80007-3_bib95","unstructured":"A. Herzig, A new decidable fragment of first order logic, June 1990 Abstracts of the 3rd Logical BiennialSummer School & Conference in honour of S. C. Kleene"},{"article-title":"Sequent Calculi for Proof Search in Some Modal Logics","year":"1996","author":"Heuerding","key":"10.1016\/S1570-2464(07)80007-3_bib96"},{"issue":"1","key":"10.1016\/S1570-2464(07)80007-3_bib97","first-page":"177","article-title":"The Logics Workbench LWB: A snapshot","volume":"2","author":"Heuerding","year":"1996","journal-title":"Euromath Bulletin"},{"key":"10.1016\/S1570-2464(07)80007-3_bib98","series-title":"Proceedings of the 5th International Workshop on Theorem Proving with Analytic Tableaux and Related Methods (TABLEAUX '96), volume 1071 of Lecture Notes in Artificial Intelligence","first-page":"210","article-title":"Efficient loop-check for backward proof search in some nonclassical propositional logics","author":"Heuerding","year":"1996"},{"key":"10.1016\/S1570-2464(07)80007-3_bib99","series-title":"Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2002), volume 2381 of Lecture Notes in Artificial Intelligence","first-page":"145","article-title":"Implementation and optimisation of a tableau algorithm for the guarded fragment","author":"Hladik","year":"2002"},{"key":"10.1016\/S1570-2464(07)80007-3_bib100","series-title":"Proceedings of the International Joint Conference on Artificial Intelligence (IJCAI-99)","first-page":"462","article-title":"A new method to index and query sets","author":"Hoffmann","year":"1999"},{"key":"10.1016\/S1570-2464(07)80007-3_bib101","series-title":"Proceedings of the 2nd Interna- tional Conference on the Principles of Knowledge Representation and Reasoning (KR '91)","first-page":"335","article-title":"Qualifying number restrictions in concept languages","author":"Hollunder","year":"1991"},{"article-title":"Optimising Tableaux Decision Procedures for Description Logics","year":"1997","author":"Horrocks","key":"10.1016\/S1570-2464(07)80007-3_bib102"},{"key":"10.1016\/S1570-2464(07)80007-3_bib103","series-title":"The Description Logic Handbook: Theory, Implementation, and Applications","first-page":"306","article-title":"Implementation and optimisation techniques","author":"Horrocks","year":"2003"},{"issue":"3","key":"10.1016\/S1570-2464(07)80007-3_bib104","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1093\/logcom\/9.3.267","article-title":"Optimizing description logic subsumption","volume":"9","author":"Horrocks","year":"1999","journal-title":"Journal of Logic and Computation"},{"issue":"3","key":"10.1016\/S1570-2464(07)80007-3_bib105","doi-asserted-by":"crossref","DOI":"10.1093\/logcom\/9.3.385","article-title":"A description logic with transitive and inverse roles and role hierarchies","volume":"9","author":"Horrocks","year":"1999","journal-title":"Journal of Logic and Computation"},{"key":"10.1016\/S1570-2464(07)80007-3_bib106","series-title":"Proceedings ofthe 17th International Joint Conference on Artificial Intelligence (IJCAI 2001)","first-page":"199","article-title":"Ontology reasoning in the SHOQ(D) description logic","author":"Horrocks","year":"2001"},{"key":"10.1016\/S1570-2464(07)80007-3_bib107","series-title":"Proceedings of the 15th European Conference on Artificial Intelligence (ECAI 2002)","first-page":"277","article-title":"Optimised reasoning for SHTQ","author":"Horrocks","year":"2002"},{"key":"10.1016\/S1570-2464(07)80007-3_bib108","series-title":"Proceedings of the 6th Int. Conf. on Logic for Programming and Auto- mated Reasoning (LPAR '99), volume 1705 of Lecture Notes in Artificial Intelligence","first-page":"161","article-title":"Practical reasoning for expressive description logics","author":"Horrocks","year":"1999"},{"key":"10.1016\/S1570-2464(07)80007-3_bib109","series-title":"Proceedings of the 7th International Conference on the Principles of Knowledge Representation and Reasoning (KR 2000)","first-page":"285","article-title":"Reasoning with axioms: Theory and practice","author":"Horrocks","year":"2000"},{"key":"10.1016\/S1570-2464(07)80007-3_bib110","series-title":"Proceedings of the 19th Interna- tional Joint Conference on Artificial Intelligence (IJCAI 2005)","first-page":"448","article-title":"A tableaux decision procedure for SHOTQ","author":"Horrocks","year":"2005"},{"article-title":"Resolution-Based Decision Procedures for Subclasses of First-Order Logic","year":"1999","author":"Hustadt","key":"10.1016\/S1570-2464(07)80007-3_bib111"},{"key":"10.1016\/S1570-2464(07)80007-3_bib112","series-title":"Proceedings of the 9th International Conference on Knowledge Representation and Reasoning (KR 2004)","first-page":"152","article-title":"Reducing SHIQ-description logic to disjunctive datalog programs","author":"Hustadt","year":"2004"},{"key":"10.1016\/S1570-2464(07)80007-3_bib113","series-title":"Proceedings ofthe 11th International Conference on Logic for Programming, Artificial Intelligence (LPAR 2004), volume 3452 of Lecture Notes in Artificial Inte","first-page":"21","article-title":"A decomposition rule for decision procedures by resolution-based calculi","author":"Hustadt","year":"2005"},{"key":"10.1016\/S1570-2464(07)80007-3_bib114","series-title":"Proceed- ings of the International Joint Conference on Artificial Intelligence (IJCAI-97)","first-page":"202","article-title":"On evaluating decision procedures for modal logic","author":"Hustadt","year":"1997"},{"key":"10.1016\/S1570-2464(07)80007-3_bib115","series-title":"Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX '98), volume 1397 of Lecture Notes in Artificial Intelligence","first-page":"187","article-title":"Simplification and backjumping in modal tableau","author":"Hustadt","year":"1998"},{"issue":"4","key":"10.1016\/S1570-2464(07)80007-3_bib116","doi-asserted-by":"crossref","first-page":"479","DOI":"10.1080\/11663081.1999.10510981","article-title":"An empirical analysis of modal theorem provers","volume":"9","author":"Hustadt","year":"1999","journal-title":"Journal of Applied Non-Classical Logics"},{"key":"10.1016\/S1570-2464(07)80007-3_bib117","series-title":"Proceedings of the 16th Inter- national Conference on Automated Deduction (CADE-16), volume 1632 of Lecture Notes in Artificial Intelligence","first-page":"172","article-title":"Maslov's class K revisited","author":"Hustadt","year":"1999"},{"key":"10.1016\/S1570-2464(07)80007-3_bib118","series-title":"Proceedings of the 16th International Joint Conference on Artificial Intelligence (IJCAI-99)","first-page":"110","article-title":"On the relation of resolution and tableaux proof systems for description logics","author":"Hustadt","year":"1999"},{"key":"10.1016\/S1570-2464(07)80007-3_bib119","series-title":"Automated Deduction in Classical and Non-Classical Logics, volume 1761 of Lecture Notes in Artificial Intelligence","first-page":"191","article-title":"Issues of decidability for description logics in the framework of resolution","author":"Hustadt","year":"2000"},{"key":"10.1016\/S1570-2464(07)80007-3_bib120","series-title":"Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2000), volume 1847 of Lecture Notes in Artificial Intelligence","first-page":"67","article-title":"MSPASS: Modal reasoning by translation and first-order resolution","author":"Hustadt","year":"2000"},{"issue":"2","key":"10.1016\/S1570-2464(07)80007-3_bib121","doi-asserted-by":"crossref","first-page":"205","DOI":"10.1023\/A:1015067300005","article-title":"Using resolution for testing modal satisfiability and building models","volume":"28","author":"Hustadt","year":"2002","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/S1570-2464(07)80007-3_bib122","first-page":"251","article-title":"A survey of decidable first-order fragments and description logics","volume":"1","author":"Hustadt","year":"2004","journal-title":"Journal of Relational Methods in Computer Science"},{"issue":"3","key":"10.1016\/S1570-2464(07)80007-3_bib123","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\/S1570-2464(07)80007-3_bib124","series-title":"Proceedings of the Second International Joint Conference on Automated Reasoning (IJCAR 2004), volume 3097 of Lecture Notes in Artificial Intelligence","first-page":"122","article-title":"A resolution decision procedure for the guarded fragment with transitive guards","author":"Kazakov","year":"2004"},{"key":"10.1016\/S1570-2464(07)80007-3_bib125","series-title":"Proceedings of the 2004 International Semantic Web Conference (ISWC2004), volume 3298 of Lecture Notes in Computer Science","first-page":"229","article-title":"The prot\u00e9g\u00e9 OWL plugin: An open development environment for semantic web applications","author":"Knublauch","year":"2004"},{"key":"10.1016\/S1570-2464(07)80007-3_bib126","series-title":"Proceedings of the 8th Inter- national Conference on Automated Deduction (CADES), volume 230 of Lecture Notes in Computer Science","first-page":"229","article-title":"Resolution and quantified epistemic logics","author":"Konolige","year":"2004"},{"year":"1999","series-title":"Tools and Techniques in Modal Logic, volume 142 of Studies in Logic and the Foundations of Mathemat- ics","author":"Kracht","key":"10.1016\/S1570-2464(07)80007-3_bib127"},{"key":"10.1016\/S1570-2464(07)80007-3_bib128","series-title":"Proceedings of the 30th ACM SIGACT Symposium on Theory of Computing (STOC-98)","first-page":"224","article-title":"Weak alternating automata and tree automata emptiness","author":"Kupferman","year":"1998"},{"issue":"3","key":"10.1016\/S1570-2464(07)80007-3_bib129","doi-asserted-by":"crossref","first-page":"467","DOI":"10.1137\/0206033","article-title":"The computational complexity of provability in systems of modal propositional logic","volume":"6","author":"Ladner","year":"1977","journal-title":"SIAM Journal of Computing"},{"key":"10.1016\/S1570-2464(07)80007-3_bib130","series-title":"Proceedings of the 24th Annual ACM symposium on Theory of Computing","first-page":"264","article-title":"Online minimization of transition systems (extended abstract)","author":"Lee","year":"1992"},{"key":"10.1016\/S1570-2464(07)80007-3_bib131","series-title":"Proceedings of the 2004 International Semantic Web Conference (ISWC 2004), volume 3298 of Lecture Notes in Computer Science","first-page":"244","article-title":"Ontotrack: Combining browsing and editing with reasoning and explaining for OWL Lite ontologies","author":"Liebig","year":"2004"},{"key":"10.1016\/S1570-2464(07)80007-3_bib132","series-title":"Proceedings of the 6th Int. Conf. on Logic for Programming and Automated Reasoning (LPAR '99), volume 1705 of Lecture Notes in Artificial Intelligence","first-page":"181","article-title":"Complexity of terminological reasoning revisited","author":"Lutz","year":"1999"},{"key":"10.1016\/S1570-2464(07)80007-3_bib133","series-title":"Proceedings of the International Joint Conference on Automated Reasoning (IJCAR-OI), volume 2083 of Lecture Notes in Artificial Intelligence","first-page":"181","article-title":"NExpTime-complete description logics with concrete domains","author":"Lutz","year":"1999"},{"key":"10.1016\/S1570-2464(07)80007-3_bib134","series-title":"Proceedings of the 1999 International Workshop on Description Logics (DL '99)","first-page":"81","article-title":"A suggestion of an n-ary description logic","author":"Lutz","year":"1999"},{"key":"10.1016\/S1570-2464(07)80007-3_bib135","series-title":"The Calculi of Symbolic Logic I: Proc. of the Steklov Institute of Mathematics edited by I. G. Petrovskiiand S. M. Nikol 'skit, Nr. 98 (1968)","first-page":"25","article-title":"The inverse method for establishing deducibility for logical calculi","author":"Maslov","year":"1971"},{"key":"10.1016\/S1570-2464(07)80007-3_bib136","series-title":"Computer-Aided Reasoning: ACL2 Case Studies","first-page":"265","article-title":"Ivy: A preprocessor and proof checker for first-order logic","author":"McCune","year":"2000"},{"key":"10.1016\/S1570-2464(07)80007-3_bib137","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1109\/5254.708435","article-title":"An industrial strength description logic-based configuration platform","author":"L. McGuinness","year":"1998","journal-title":"IEEE Intelligent Systems"},{"key":"10.1016\/S1570-2464(07)80007-3_bib138","series-title":"Proceedings of the Thirteenth International World Wide Web Conference (WWW 2004)","first-page":"563","article-title":"Foundations for service ontologies: Aligning OWL-S to dolce","author":"Mika","year":"2004"},{"key":"10.1016\/S1570-2464(07)80007-3_bib139","series-title":"Proceedings of COLOG-88, volume 417 of Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"198","DOI":"10.1007\/3-540-52335-9_55","article-title":"Gentzen-type systems and resolution rules. Part I: Propositional lo gic","author":"Mints","year":"1990"},{"key":"10.1016\/S1570-2464(07)80007-3_bib140","series-title":"Proof Theory of Modal Logic, volume 2 of Applied Logic Series","first-page":"17","article-title":"Transfer of sequent calculus strategies to resolution for S4","author":"Mints","year":"1996"},{"key":"10.1016\/S1570-2464(07)80007-3_bib141","unstructured":"L.Nguyen. MProlog. http:\/\/www.mimuw.edu.pl\/~nguyen\/mprolog\/."},{"issue":"1","key":"10.1016\/S1570-2464(07)80007-3_bib142","first-page":"63","article-title":"A fixpoint semantics and an sld-resolution calculus for modal logic programs","volume":"55","author":"Nguyen","year":"2003","journal-title":"Fundamenta Informaticae"},{"key":"10.1016\/S1570-2464(07)80007-3_bib143","series-title":"Proceedings of the 9th European Conference on Logics in Artificial Intelligence (JELIA 2004), volume 3229 of Lecture Notes in Artificial Intelligence","first-page":"266","article-title":"The modal logic programming system MProlog","author":"Nguyen","year":"2004"},{"key":"10.1016\/S1570-2464(07)80007-3_bib144","series-title":"Proceedings of the 5th International Workshop on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX '96), volume 1071 of Lecture Notes in Artificial Intelligence","first-page":"266","article-title":"A tableau calculus for minimal model reasoning","author":"Niemel\u00e4","year":"2004"},{"key":"10.1016\/S1570-2464(07)80007-3_bib145","series-title":"Proceedings of the 13th International Joint Conference on Artificial Intelligence (IJCAI-93)","first-page":"80","article-title":"First-order modal logic theorem proving and functional simulation","author":"Nonnengart","year":"1993"},{"key":"10.1016\/S1570-2464(07)80007-3_bib146","series-title":"Proceedings of the European Workshop on Logics in Artificial Intelligence (JELIA '94), volume 838 of Lecture Notes in Artificial Intelligence","first-page":"365","article-title":"How to use modalities and sorts in prolog","author":"Nonnengart","year":"1994"},{"key":"10.1016\/S1570-2464(07)80007-3_bib147","unstructured":"A. Nonnengart, H. J. Ohlbach, and A. Szalas. Quantifier elimination for second-order predicate logic. To appear in Logic, Language and Reasoning: Essays in honour of Dov Gabbay, Part I, Kluwer."},{"key":"10.1016\/S1570-2464(07)80007-3_bib148","first-page":"1403","article-title":"Encoding two-valued nonclassical logics in classical logic","volume":"volume II","author":"Ohlbach","year":"2001"},{"issue":"5","key":"10.1016\/S1570-2464(07)80007-3_bib149","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\/S1570-2464(07)80007-3_bib150","series-title":"Proof Theory of Modal Logic, volume 2 of Applied Logic Series","first-page":"253","article-title":"Translating graded modalities into predicate logic","author":"Ohlbach","year":"1996"},{"key":"10.1016\/S1570-2464(07)80007-3_bib151","first-page":"113","article-title":"Gentzen method in modal calculi","volume":"9","author":"Ohnishi","year":"1957","journal-title":"Osaka Mathematical Journal"},{"key":"10.1016\/S1570-2464(07)80007-3_bib152","first-page":"115","article-title":"Gentzen method in modal calculi II","volume":"11","author":"Ohnishi","year":"1959","journal-title":"Osaka Mathematical Journal"},{"key":"10.1016\/S1570-2464(07)80007-3_bib153","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"},{"key":"10.1016\/S1570-2464(07)80007-3_bib154","series-title":"Proceedings of the First International Conference on Temporal Logic (ICTL '94), volume 827 of Lecture Notes in Artificial Intelligence","first-page":"445","article-title":"An overview of temporal and modal logic programming","author":"Orgun","year":"1994"},{"key":"10.1016\/S1570-2464(07)80007-3_bib155","series-title":"Proceedings of the 8th International Conference on Computer-Aided Verification (CAV '96), volume 1102 of Lecture Notes in Computer Science","first-page":"411","article-title":"PVS: Combining specification, proof checking, and model checking","author":"Owre","year":"1996"},{"issue":"6","key":"10.1016\/S1570-2464(07)80007-3_bib156","doi-asserted-by":"crossref","first-page":"973","DOI":"10.1137\/0216062","article-title":"Three partition refinement algorithms","volume":"16","author":"Paige","year":"1987","journal-title":"SIAM Journal on Computing"},{"key":"10.1016\/S1570-2464(07)80007-3_bib157","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1016\/0304-3975(85)90159-8","article-title":"A linear time solution to the single function coarsest partition problem","volume":"40","author":"Paige","year":"1985","journal-title":"Theo- retical Computer Science"},{"key":"10.1016\/S1570-2464(07)80007-3_bib158","series-title":"Proceedings of the 19th Inter- national Conference on Automated Deduction (CADE-19), volume 2741 of Lecture Notes in Artificial Intelligence","first-page":"75","article-title":"Optimizing a BDD-based modal solver","author":"Pan","year":"2003"},{"key":"10.1016\/S1570-2464(07)80007-3_bib159","series-title":"Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX '99), volume 1397 of Lecture Notes in Artificial Intelligence","first-page":"19","article-title":"DLP and FaCT","author":"Patel-Schneider","year":"1999"},{"year":"2003","series-title":"Maryland Information and Network Dynamics Lab","author":"Pellet","key":"10.1016\/S1570-2464(07)80007-3_bib160"},{"key":"10.1016\/S1570-2464(07)80007-3_bib161","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1016\/S0747-7171(86)80028-1","article-title":"A structure-preserving clause form translation","volume":"2","author":"Plaisted","year":"1986","journal-title":"Journal of Symbolic Computation"},{"key":"10.1016\/S1570-2464(07)80007-3_bib162","series-title":"Proceedings of the 20th Annual Symposium on Foundations of Computer Science","article-title":"Models of program logics","author":"Pratt","year":"1979"},{"year":"1967","series-title":"Past, Present and Future","author":"Prior","key":"10.1016\/S1570-2464(07)80007-3_bib163"},{"issue":"3","key":"10.1016\/S1570-2464(07)80007-3_bib164","doi-asserted-by":"crossref","first-page":"268","DOI":"10.1111\/j.1467-8640.1993.tb00310.x","article-title":"Hybrid algorithms for the constraint satisfaction problem","volume":"9","author":"Prosser","year":"1979","journal-title":"Computational Intelligence"},{"key":"10.1016\/S1570-2464(07)80007-3_bib165","first-page":"343","article-title":"Variables explained away","volume":"volume 104","author":"Quine","year":"1960","journal-title":"Proceedings of the American Philosophy Society"},{"key":"10.1016\/S1570-2464(07)80007-3_bib166","series-title":"Logic and Art: Esssays in Honor of Nelson Goodman","article-title":"Algebraic logic and predicate functors","author":"Quine","year":"1971"},{"key":"10.1016\/S1570-2464(07)80007-3_bib167","series-title":"Proceedings of the 17th Annual Symposium on Computer Applications in Medical Care (SCAMC '93)","first-page":"414","article-title":"Goals for concept representation in the GALEN project","author":"Rector","year":"1993"},{"key":"10.1016\/S1570-2464(07)80007-3_bib168","series-title":"Proceedings of the 17th Interna- tional Joint Conference on Artificial Intelligence (IJCAI 2001)","first-page":"611","article-title":"Splitting without backtracking","author":"Riazanov","year":"2001"},{"issue":"2\u20133","key":"10.1016\/S1570-2464(07)80007-3_bib169","first-page":"91","article-title":"The design and implementation of Vampire","volume":"15","author":"Riazanov","year":"2002","journal-title":"AI Communications"},{"key":"10.1016\/S1570-2464(07)80007-3_bib170","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":"Journal of the ACM"},{"key":"10.1016\/S1570-2464(07)80007-3_bib171","series-title":"Proceedings of the 14th European Conference on Artificial Intelligence (ECAI 2000)","first-page":"239","article-title":"Description logics for the representation of aggregated objects","author":"Sattler","year":"2000"},{"key":"10.1016\/S1570-2464(07)80007-3_bib172","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1016\/S0022-0000(70)80006-X","article-title":"Relationsship between nondeterministic and deterministic tape complexities","volume":"4","author":"Savitch","year":"1970","journal-title":"Journal of Computer and System Science"},{"key":"10.1016\/S1570-2464(07)80007-3_bib173","series-title":"Proceedings of the 12th International Joint Conference on Artificial Intelligence (IJCAI-91)","first-page":"466","article-title":"A correspondence theory for terminological logics: Preliminary report","author":"Schild","year":"1991"},{"key":"10.1016\/S1570-2464(07)80007-3_bib174","unstructured":"R.A.Schmidt. MSPASS. http:\/\/www.cs.man.ac.uk\/~schmidt\/mspass."},{"article-title":"Optimised Modal Translation and Resolution","year":"1997","author":"Schmidt","key":"10.1016\/S1570-2464(07)80007-3_bib175"},{"key":"10.1016\/S1570-2464(07)80007-3_bib176","series-title":"Proceedings of the 9th International Conference on Rewriting Techniques and Applications (RTA '98), volume 1379 of Lecture Notes in Computer Science","first-page":"106","article-title":"E-unification for subsystems of S4","author":"Schmidt","year":"1998"},{"issue":"4","key":"10.1016\/S1570-2464(07)80007-3_bib177","doi-asserted-by":"crossref","first-page":"379","DOI":"10.1023\/A:1006043519663","article-title":"Decidability by resolution for propositional modal logics","volume":"22","author":"Schmidt","year":"1999","journal-title":"Journal of Automated Reasoning"},{"issue":"4","key":"10.1016\/S1570-2464(07)80007-3_bib178","doi-asserted-by":"crossref","first-page":"379","DOI":"10.1023\/A:1006043519663","article-title":"Decidability by resolution for propositional modal logics","volume":"22","author":"Schmidt","year":"1999","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/S1570-2464(07)80007-3_bib179","series-title":"Proceedings of the 17th International Conference on Automated Deduction (CADE-17), volume 1831 of Lecture Notes in Artificial Intelligence","first-page":"433","article-title":"A resolution decision procedure for fluted logic","author":"Schmidt","year":"2000"},{"key":"10.1016\/S1570-2464(07)80007-3_bib180","series-title":"Theory and Applications of Relational Structures as Knowledge Instruments, volume 2929 of Lecture Notes in Computer Science","first-page":"38","article-title":"Mechanised reasoning and model generation for extended modal logics","author":"Schmidt","year":"2003"},{"key":"10.1016\/S1570-2464(07)80007-3_bib181","series-title":"Proceedings of the 19th International Conference on Automated Deduction (CADE-19), volume 2741 of Lecture Notes in Artificial Intelligence","first-page":"412","article-title":"A principle for incorporating axioms into the first-order translation of modal formulae","author":"Schmidt","year":"2003"},{"key":"10.1016\/S1570-2464(07)80007-3_bib182","series-title":"Volume in memoriam of Harald Ganzinger, Lecture Notes in Computer Science","article-title":"First-order resolution methods for modal logics","author":"Schmidt","year":"2006"},{"issue":"2\/3","key":"10.1016\/S1570-2464(07)80007-3_bib183","first-page":"111","article-title":"E: A Brainiac theorem prover","volume":"15","author":"Schulz","year":"2002","journal-title":"Journal of AI Communications"},{"article-title":"Complexity of Modal Logics","year":"1993","author":"Spaan","key":"10.1016\/S1570-2464(07)80007-3_bib184"},{"issue":"6","key":"10.1016\/S1570-2464(07)80007-3_bib185","doi-asserted-by":"crossref","first-page":"605","DOI":"10.1093\/logcom\/3.6.605","article-title":"On the correspondence between modal and classical logic: An automated approach","volume":"3","author":"Szalas","year":"1993","journal-title":"Journal of Logic and Computation"},{"article-title":"Complexity Results and Practical Algorithms for Logics in Knowledge Representation","year":"2001","author":"Tobies","key":"10.1016\/S1570-2464(07)80007-3_bib186"},{"key":"10.1016\/S1570-2464(07)80007-3_bib187","first-page":"241","article-title":"Temporal logic","volume":"Volume 4","author":"van Benthem","year":"1996"},{"key":"10.1016\/S1570-2464(07)80007-3_bib188","series-title":"Proceedings of the 25th Int. Colloq. on Automata, Languages, and Programming, volume 1443 of Lecture Notes in Computer Science","first-page":"628","article-title":"Reasoning about the past with two-way automata","author":"Vardi","year":"1998"},{"issue":"1","key":"10.1016\/S1570-2464(07)80007-3_bib189","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1016\/S0098-3004(01)00019-X","article-title":"Ontologies for geographic information processing","volume":"28","author":"Visser","year":"2002","journal-title":"Com- puters & Geosciences"},{"key":"10.1016\/S1570-2464(07)80007-3_bib190","series-title":"Proceedings of the 11th Conference on Automated Deduction (CADE-11), volume 607 of Lecture Notes in Artificial Intelligence","first-page":"648","article-title":"Theorem proving in non-standard logics based on the inverse method","author":"Voronkov","year":"1992"},{"article-title":"An abstract prolog instruction set","year":"1983","author":"Wan-en","key":"10.1016\/S1570-2464(07)80007-3_bib191"},{"key":"10.1016\/S1570-2464(07)80007-3_bib192","unstructured":"C. Weidenbach. SPASS. http:\/\/spass.mpi-sb.mpg.de."},{"key":"10.1016\/S1570-2464(07)80007-3_bib193","first-page":"1965","article-title":"Combining superposition, sorts and splitting","volume":"volume II","author":"Weidenbach","year":"2001"},{"key":"10.1016\/S1570-2464(07)80007-3_bib194","series-title":"Proceedings of the 16th In- ternational Conference on Automated Deduction (CADE-16), volume 1632 of Lecture Notes in Artificial Intelligence","first-page":"378","article-title":"System description: Spass version 1.0.0","author":"Weidenbach","year":"1999"},{"issue":"2","key":"10.1016\/S1570-2464(07)80007-3_bib195","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1023\/A:1008643803725","article-title":"Validation of HOL proofs by proof checking","volume":"14","author":"Wong","year":"1999","journal-title":"Formal Methods in System Design"},{"year":"2000","series-title":"Reasoning about rational agents","author":"Wooldridge","key":"10.1016\/S1570-2464(07)80007-3_bib196"},{"issue":"2","key":"10.1016\/S1570-2464(07)80007-3_bib197","doi-asserted-by":"crossref","first-page":"597","DOI":"10.1142\/S0218843003000711","article-title":"A suite of DAML+OIL ontologies to describe bioinformatics web services and data","volume":"12","author":"Wroe","year":"2003","journal-title":"International Journal of Cooperative Information Systems"}],"container-title":["Studies in Logic and Practical Reasoning","Handbook of Modal Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1570246407800073?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1570246407800073?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T23:15:40Z","timestamp":1761606940000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1570246407800073"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007]]},"ISBN":["9780444516909"],"references-count":200,"URL":"https:\/\/doi.org\/10.1016\/s1570-2464(07)80007-3","relation":{},"ISSN":["1570-2464"],"issn-type":[{"type":"print","value":"1570-2464"}],"subject":[],"published":{"date-parts":[[2007]]}}}