{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,9]],"date-time":"2026-04-09T12:14:10Z","timestamp":1775736850132,"version":"3.50.1"},"reference-count":145,"publisher":"Elsevier","isbn-type":[{"value":"9780444516909","type":"print"}],"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)80017-6","type":"book-chapter","created":{"date-parts":[[2007,10,4]],"date-time":"2007-10-04T09:38:50Z","timestamp":1191490730000},"page":"821-868","source":"Crossref","is-referenced-by-count":123,"title":["14 Hybrid logics"],"prefix":"10.1016","member":"78","reference":[{"key":"10.1016\/S1570-2464(07)80017-6_bib1","series-title":"Words, Proofs, and Diagrams","first-page":"5","article-title":"Logical Patterns in Space","author":"Aiello","year":"2002"},{"issue":"2","key":"10.1016\/S1570-2464(07)80017-6_bib2","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1016\/0004-3702(84)90008-0","article-title":"Towards a general theory of action and time","volume":"23","author":"Allen","year":"1984","journal-title":"Artificial Intelligence"},{"key":"10.1016\/S1570-2464(07)80017-6_bib3","unstructured":"C. Areces. HyLo: The hybrid logics' web site, http : \/ \/hylo. loria. f r. Last visited: Dec\/05."},{"key":"10.1016\/S1570-2464(07)80017-6_bib4","article-title":"Logic Engineering. The Case of Description and Hybrid Logics","author":"Areces","year":"2000"},{"key":"10.1016\/S1570-2464(07)80017-6_bib5","series-title":"Methods for Modalities 3","year":"2003"},{"key":"10.1016\/S1570-2464(07)80017-6_bib6","series-title":"Computer Science Logic. Proceedings of the 8th Annual Conference of the EACSL number 1683 in LNCS","first-page":"307","article-title":"A road-map on complexity for hybrid logics","author":"Areces","year":"1999"},{"issue":"5","key":"10.1016\/S1570-2464(07)80017-6_bib7","doi-asserted-by":"crossref","first-page":"653","DOI":"10.1093\/jigpal\/8.5.653","article-title":"The computational complexity of hybrid temporal logics","volume":"8","author":"Areces","year":"2000","journal-title":"Logic Journal of the IGPL"},{"issue":"3","key":"10.1016\/S1570-2464(07)80017-6_bib8","doi-asserted-by":"crossref","first-page":"977","DOI":"10.2307\/2695090","article-title":"Hybrid logics: Characterization, interpolation and complexity","volume":"66","author":"Areces","year":"2001","journal-title":"Journal of Symbolic Logic"},{"issue":"1-3","key":"10.1016\/S1570-2464(07)80017-6_bib9","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1016\/S0168-0072(03)00059-9","article-title":"Repairing the interpolation lemma in quantified modal logic","volume":"123","author":"Areces","year":"2003","journal-title":"Annals of Purend Applied Logics"},{"key":"10.1016\/S1570-2464(07)80017-6_bib10","series-title":"Automated Deduction\u2014CADE-16 (Trento, 1999)","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)80017-6_bib11","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 andComputation"},{"key":"10.1016\/S1570-2464(07)80017-6_bib12","first-page":"17","article-title":"From description to hybrid logics, and back","volume":"Volume 3","author":"Areces","year":"2001"},{"key":"10.1016\/S1570-2464(07)80017-6_bib13","series-title":"Methods for Modalities 1","volume":"8","year":"2000"},{"key":"10.1016\/S1570-2464(07)80017-6_bib14","first-page":"125","article-title":"Ordered resolution with selection for h(@)","volume":"volume 3452","author":"Areces","year":"2005"},{"key":"10.1016\/S1570-2464(07)80017-6_bib15","unstructured":"C. Areces, J. Heguiabehere, D. Gorin, HyLoRes A hybrid logic resolution system http:\/\/www. loria. fr\/~areces\/HyLoRes. Last visited: Dec\/05"},{"key":"10.1016\/S1570-2464(07)80017-6_bib16","series-title":"The Description Logic Handbook: Theory, implementation and applications","year":"2003"},{"key":"10.1016\/S1570-2464(07)80017-6_bib17","first-page":"19","article-title":"Resolution theorem proving","volume":"Volume 1","author":"Bachmair","year":"2001"},{"key":"10.1016\/S1570-2464(07)80017-6_bib18","series-title":"Admissible Sets and Structures","author":"Barwise","year":"1975"},{"issue":"1","key":"10.1016\/S1570-2464(07)80017-6_bib19","doi-asserted-by":"crossref","DOI":"10.1093\/jigpal\/4.1.23","article-title":"Modal logics for qualitative spatial reasoning","volume":"4","author":"Bennett","year":"1996","journal-title":"Logic Journal of the IGPL"},{"issue":"2","key":"10.1016\/S1570-2464(07)80017-6_bib20","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1093\/logcom\/exi056","article-title":"Transfer results for hybrid logic. Part I: the case without satisfaction operators","volume":"16","author":"Bezhanishvili","year":"2006","journal-title":"Journal of Logic and Computation"},{"key":"10.1016\/S1570-2464(07)80017-6_bib21","series-title":"Nominal Tense Logic and Other Sorted Intensional Frameworks","author":"Blackburn","year":"1990"},{"issue":"1","key":"10.1016\/S1570-2464(07)80017-6_bib22","doi-asserted-by":"crossref","first-page":"56","DOI":"10.1305\/ndjfl\/1093634564","article-title":"Nominal tense logic","volume":"34","author":"Blackburn","year":"1992","journal-title":"Notre Dame Journal of Formal Logic"},{"key":"10.1016\/S1570-2464(07)80017-6_bib23","series-title":"Diamonds and Defaults","first-page":"19","article-title":"Modal logic and attribute value structures","author":"Blackburn","year":"1993"},{"key":"10.1016\/S1570-2464(07)80017-6_bib24","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1093\/jos\/11.1-2.83","article-title":"Tense, temporal reference and tense logic","volume":"11","author":"Blackburn","year":"1994","journal-title":"Journal of Semantics"},{"key":"10.1016\/S1570-2464(07)80017-6_bib25","doi-asserted-by":"crossref","first-page":"136","DOI":"10.1093\/logcom\/10.1.137","article-title":"Internalizing labelled deduction","volume":"10","author":"Blackburn","year":"2000","journal-title":"Journal of Logic and Computation"},{"key":"10.1016\/S1570-2464(07)80017-6_bib26","doi-asserted-by":"crossref","unstructured":"P. Blackburn, Representation, reasoning, and relational structures: a Hybrid Logic manifesto Areces, 339-365, Appeared as a Special Issue of the Logic Journal of the IGPL, 8, (3)","DOI":"10.1093\/jigpal\/8.3.339"},{"key":"10.1016\/S1570-2464(07)80017-6_bib27","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1023\/A:1010358017657","article-title":"Modal logic as dialogical logic","volume":"127","author":"Blackburn","year":"2001","journal-title":"Synthese"},{"key":"10.1016\/S1570-2464(07)80017-6_bib28","series-title":"Modal Logic","author":"Blackburn","year":"2001"},{"key":"10.1016\/S1570-2464(07)80017-6_bib29","first-page":"38","article-title":"Tableaux for quantified hybrid logic","volume":"volume 2381","author":"Blackburn","year":"2002"},{"issue":"2","key":"10.1016\/S1570-2464(07)80017-6_bib30","doi-asserted-by":"crossref","first-page":"463","DOI":"10.2178\/jsl\/1052669059","article-title":"Constructive interpolation in hybrid logic","volume":"68","author":"Blackburn","year":"2003","journal-title":"The Journal of Symbolic Logic"},{"issue":"3","key":"10.1016\/S1570-2464(07)80017-6_bib31","doi-asserted-by":"crossref","first-page":"251","DOI":"10.1007\/BF01049415","article-title":"Hybrid languages","volume":"4","author":"Blackburn","year":"1995","journal-title":"Journal of Logic, Language and Information"},{"key":"10.1016\/S1570-2464(07)80017-6_bib32","series-title":"Advances in Modal Logic 1","first-page":"41","article-title":"What are hybrid languages?","author":"Blackburn","year":"1998"},{"key":"10.1016\/S1570-2464(07)80017-6_bib33","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1007\/BF01050635","article-title":"A modal perspective on the computational complexity of attribute value grammar","volume":"2","author":"Blackburn","year":"1993","journal-title":"Journal of Logic, Language and Information"},{"key":"10.1016\/S1570-2464(07)80017-6_bib34","unstructured":"P. Blackburn, B. ten Cate Pure extensions, proof rules, and hybrid axiomatics, 127, Schmidt, 19-29"},{"key":"10.1016\/S1570-2464(07)80017-6_bib35","doi-asserted-by":"crossref","first-page":"625","DOI":"10.1093\/jigpal\/6.4.625","article-title":"Hybrid completeness","volume":"6","author":"Blackburn","year":"1998","journal-title":"Logic Journal of the IGPL"},{"key":"10.1016\/S1570-2464(07)80017-6_bib36","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1023\/A:1018988913388","article-title":"Hybridizing concept languages","volume":"24","author":"Blackburn","year":"1998","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"issue":"1","key":"10.1016\/S1570-2464(07)80017-6_bib37","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1093\/jigpal\/7.1.27","article-title":"Hybrid languages and temporal logic","volume":"7","author":"Blackburn","year":"1999","journal-title":"Logic Journal of the IGPL"},{"key":"10.1016\/S1570-2464(07)80017-6_bib38","unstructured":"T. Bolander and T. Bra\u00fcner. Two tableau-based decision procedures for hybrid logic. In Schlinglof [126]."},{"key":"10.1016\/S1570-2464(07)80017-6_bib39","series-title":"The Classical Decision Problem","author":"Borger","year":"1997"},{"key":"10.1016\/S1570-2464(07)80017-6_bib40","doi-asserted-by":"crossref","first-page":"277","DOI":"10.1613\/jair.56","article-title":"A semantics and complete algorithm for subsumption in the CLASSIC description logic","volume":"1","author":"Borgida","year":"1994","journal-title":"Journal of Artificial Intelligence Research"},{"issue":"2","key":"10.1016\/S1570-2464(07)80017-6_bib41","first-page":"171","article-title":"An overview of the KL-ONE knowledge representation system","volume":"9","author":"Brachman","year":"1985","journal-title":"Cognitive Science"},{"issue":"3","key":"10.1016\/S1570-2464(07)80017-6_bib42","doi-asserted-by":"crossref","first-page":"329","DOI":"10.1093\/logcom\/14.3.329","article-title":"Natural deduction for hybrid logic","volume":"14","author":"Bra\u00fcner","year":"2004","journal-title":"Journal of Logic and Computation"},{"issue":"1","key":"10.1016\/S1570-2464(07)80017-6_bib43","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1023\/A:1026187215321","article-title":"Two natural deduction systems for hybrid logic: A comparison","volume":"13","author":"Bra\u00fcner","year":"2004","journal-title":"Journal of Logic, Language and Infor- mation"},{"issue":"2","key":"10.1016\/S1570-2464(07)80017-6_bib44","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1007\/s10849-005-3927-y","article-title":"Natural deduction for first-order hybrid logic","volume":"14","author":"Bra\u00fcner","year":"2005","journal-title":"Journal of Logic, Language and Information"},{"key":"10.1016\/S1570-2464(07)80017-6_bib45","unstructured":"T. Bra\u00fcner and V. de Paiva. Towards constructive hybrid logic. In Areces and Blackburn [5]."},{"key":"10.1016\/S1570-2464(07)80017-6_bib46","doi-asserted-by":"crossref","first-page":"282","DOI":"10.1111\/j.1755-2567.1970.tb00428.x","article-title":"An approach to tense logic","volume":"36","author":"Bull","year":"1970","journal-title":"Theoria"},{"key":"10.1016\/S1570-2464(07)80017-6_bib47","series-title":"Logic and Computa- tion","first-page":"67","article-title":"Bounded arithmetic and propositional proof complexity","author":"Buss","year":"1997"},{"key":"10.1016\/S1570-2464(07)80017-6_bib48","series-title":"Proceedings of the 16th International Joint Conference on Artificial Intelligence (IJCAI'99)","first-page":"84","article-title":"Reasoning in expressive description logics with fixpoints based on automata on infinite trees","author":"Calvanese","year":"1999"},{"key":"10.1016\/S1570-2464(07)80017-6_bib49","series-title":"Modal logic","author":"Chagrov","year":"1997"},{"key":"10.1016\/S1570-2464(07)80017-6_bib50","series-title":"Proceedings of the Third International Symposium on Logical Foundations of Computer Science","first-page":"69","article-title":"The complexity of prepositional modal theories and the complexity of consistency of prepositional modal theories","volume":"volume 813","author":"Chen","year":"1994"},{"key":"10.1016\/S1570-2464(07)80017-6_bib51","series-title":"The Stanford Encyclopedia of Philosophy","author":"Copeland","year":"1999"},{"key":"10.1016\/S1570-2464(07)80017-6_bib52","series-title":"Entities and Indices","author":"Cresswell","year":"1990"},{"key":"10.1016\/S1570-2464(07)80017-6_bib53","series-title":"Semantic Indexicality","author":"Cresswell","year":"1996"},{"key":"10.1016\/S1570-2464(07)80017-6_bib54","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1016\/0168-0072(95)00016-X","article-title":"Topological reasoning and the logic of knowledge","volume":"78","author":"Dabrowski","year":"1996","journal-title":"Annals of Pure and Applied Logic"},{"key":"10.1016\/S1570-2464(07)80017-6_bib55","article-title":"Decidability of class-based knowledge representation formalisms","author":"De Giacomo","year":"1995"},{"key":"10.1016\/S1570-2464(07)80017-6_bib56","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 prepositional dy-namic logics","author":"De Giacomo","year":"1994"},{"key":"10.1016\/S1570-2464(07)80017-6_bib57","first-page":"140","article-title":"Sequent calculi for nominal tense logics: a step towards mechanization?","volume":"volume 1617","author":"Demri","year":"1999"},{"key":"10.1016\/S1570-2464(07)80017-6_bib58","series-title":"A mathematical introduction to logic","author":"Enderton","year":"1972"},{"key":"10.1016\/S1570-2464(07)80017-6_bib59","first-page":"29","article-title":"Persistent and invariant formulas for outer extensions","volume":"20","author":"Feferman","year":"1968","journal-title":"Compositio Mathematica"},{"key":"10.1016\/S1570-2464(07)80017-6_bib60","doi-asserted-by":"crossref","first-page":"480","DOI":"10.1090\/S0002-9904-1966-11507-0","article-title":"Persistent and invariant formulas relative to theories of higher order","volume":"72","author":"Feferman","year":"1966","journal-title":"Bulletin of the American Mathematical Society"},{"key":"10.1016\/S1570-2464(07)80017-6_bib61","doi-asserted-by":"crossref","first-page":"336","DOI":"10.1111\/j.1755-2567.1970.tb00432.x","article-title":"Prepositional quantifiers in modal logic","volume":"36","author":"Fine","year":"1970","journal-title":"Theoria"},{"issue":"2","key":"10.1016\/S1570-2464(07)80017-6_bib62","doi-asserted-by":"crossref","first-page":"201","DOI":"10.2307\/2273727","article-title":"Failures of the interpolation lemma in quantified modal logic","volume":"44","author":"Fine","year":"1979","journal-title":"Journal of Symbolic Logic"},{"key":"10.1016\/S1570-2464(07)80017-6_bib63","series-title":"First order logic and automated theorem proving","author":"Fitting","year":"1996"},{"key":"10.1016\/S1570-2464(07)80017-6_bib64","unstructured":"M. Franceschet, M. de Rijke, Model checking for hybrid logics, Areces and Blackburn [5], pages 109-124"},{"key":"10.1016\/S1570-2464(07)80017-6_bib65","series-title":"Proceedings of the 10th International Symposium on Temporal Representation and Reasoning \/ 4th International Conference on Temporal Logic (TIME-ICTL 2003)","first-page":"166","article-title":"Hybrid logics on linear structures: Expressivity and complexity","author":"Franceschet","year":"2003"},{"key":"10.1016\/S1570-2464(07)80017-6_bib66","series-title":"Investigations in Modal and Tense Logics with Applications to Problems in Philosophy and Linguistics","author":"Gabbay","year":"1976"},{"key":"10.1016\/S1570-2464(07)80017-6_bib67","series-title":"Aspects of Philosophical Logic","first-page":"67","author":"Gabbay","year":"1981"},{"key":"10.1016\/S1570-2464(07)80017-6_bib68","volume":"Vol. 1","author":"Gabbay","year":"1996"},{"key":"10.1016\/S1570-2464(07)80017-6_bib69","volume":"volume 148","author":"Gabbay","year":"2003"},{"key":"10.1016\/S1570-2464(07)80017-6_bib70","article-title":"Modal definability in topology","author":"Gabelaia","year":"2001"},{"key":"10.1016\/S1570-2464(07)80017-6_bib71","series-title":"Mathematical Theory of Programming","first-page":"42","article-title":"Decidability of the basic combinatory prepositional dynamic logic (in Russian)","author":"Gargov","year":"1985"},{"issue":"6","key":"10.1016\/S1570-2464(07)80017-6_bib72","doi-asserted-by":"crossref","first-page":"607","DOI":"10.1007\/BF01054038","article-title":"Modal logic with names","volume":"22","author":"Gargov","year":"1993","journal-title":"Journal of Philosophical Logic"},{"issue":"2\u20133","key":"10.1016\/S1570-2464(07)80017-6_bib73","article-title":"Determinism and looping in combinatory PDL","volume":"61","author":"Gargov","year":"1985","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1570-2464(07)80017-6_bib74","series-title":"Mathemat- ical Logic and its Applications","first-page":"253","article-title":"Modal environment for boolean speculations","author":"Gargov","year":"1987"},{"key":"10.1016\/S1570-2464(07)80017-6_bib75","series-title":"Axiomatizing the Logic of Computer Programming","author":"Goldblatt","year":"1982"},{"key":"10.1016\/S1570-2464(07)80017-6_bib76","series-title":"Algebra andLogic","first-page":"163","article-title":"Axiomatic classes in prepositional modal logic","author":"Goldblatt","year":"1974"},{"key":"10.1016\/S1570-2464(07)80017-6_bib77","first-page":"133","article-title":"Temporal logic with reference pointers","volume":"volume 827","author":"Goranko","year":"1994"},{"issue":"1","key":"10.1016\/S1570-2464(07)80017-6_bib78","first-page":"1","article-title":"Hierarchies of modal and temporal logics with reference pointers","volume":"5","author":"Goranko","year":"1996","journal-title":"Journal of Logic, Language andInformation"},{"issue":"3\u20134","key":"10.1016\/S1570-2464(07)80017-6_bib79","first-page":"221","article-title":"Computation tree logics and temporal logics with reference pointers","volume":"10","author":"Goranko","year":"2000","journal-title":"Journal of Applied Non-classicalLogics"},{"issue":"5","key":"10.1016\/S1570-2464(07)80017-6_bib80","doi-asserted-by":"crossref","first-page":"737","DOI":"10.1093\/logcom\/11.5.737","article-title":"Sahlqvist formulae in hybrid polyadic modal logics","volume":"ll","author":"Goranko","year":"2001","journal-title":"Journal of Logic and Computation"},{"key":"10.1016\/S1570-2464(07)80017-6_bib81","series-title":"Proceedings of the 5th Internaltion Joint Conference on AutomatedReasoning (IJCAR'01) number 2083","year":"2001"},{"issue":"4","key":"10.1016\/S1570-2464(07)80017-6_bib82","doi-asserted-by":"crossref","first-page":"1719","DOI":"10.2307\/2586808","article-title":"On the restraining power of guards","volume":"64","author":"Gr\u00e4del","year":"1999","journal-title":"Journal of Symbolic Logic"},{"key":"10.1016\/S1570-2464(07)80017-6_bib83","unstructured":"V. Haarslev and R. M\u00f6ller. RACER: Renamed ABox and concept expression reasoner. http:\/\/www.sts. tu-harburg.de\/~r. f.moeller\/racer. Last visited: Dec\/05"},{"key":"10.1016\/S1570-2464(07)80017-6_bib84","doi-asserted-by":"crossref","unstructured":"V. Haarslev and R. M\u00f6ller. RACER system description. In Gor\u00e9 et al. [81], pages 701-705.","DOI":"10.1007\/3-540-45744-5_59"},{"key":"10.1016\/S1570-2464(07)80017-6_bib85","first-page":"497","article-title":"Dynamic logic","volume":"volume165","author":"Harel","year":"1984"},{"key":"10.1016\/S1570-2464(07)80017-6_bib86","first-page":"181","article-title":"A hybrid logic of knowledge supporting topological reasoning","volume":"volume 3116","author":"Heinemann","year":"2004"},{"issue":"3","key":"10.1016\/S1570-2464(07)80017-6_bib87","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1093\/jigpal\/12.3.181","article-title":"The hybrid logic of linear set spaces","volume":"12","author":"Heinemann","year":"2004","journal-title":"Logic Journal of the IGPL"},{"key":"10.1016\/S1570-2464(07)80017-6_bib88","series-title":"PODC '90: Proceedings of the 9thannual ACM Symposium on Principles of Distributed Computing","first-page":"281","article-title":"Half-order modal logic: how to prove real-time properties","author":"Henzinger","year":"1990"},{"key":"10.1016\/S1570-2464(07)80017-6_bib89","unstructured":"I. Horrocks. FaCT: Fast classification of terminologies. http:\/\/www.cs.man.ac.uk\/~horrocks\/FaCT. Last visited: Dec\/05."},{"key":"10.1016\/S1570-2464(07)80017-6_bib90","series-title":"Proceedings of the 6th International Conference on the Principles of Knowledge Representation and Reasoning (KR98)","first-page":"636","article-title":"Using an expressive description logic: FaCT or fiction?","author":"Horrocks","year":"1998"},{"key":"10.1016\/S1570-2464(07)80017-6_bib91","series-title":"Proceedingsof the 17th International Joint Conference on Artificial Intelligence (IJCAI'01)","first-page":"199","article-title":"Ontology reasoning in the SHOQ(D) description logic","author":"Horrocks","year":"2001"},{"key":"10.1016\/S1570-2464(07)80017-6_bib92","series-title":"Proceedings of the 17th International Joint Conference on Artificial Intelligence (IJCAI'01)","first-page":"199","article-title":"A tableaux decision procedure for SHOIQ","author":"Horrocks","year":"2005"},{"key":"10.1016\/S1570-2464(07)80017-6_bib93","doi-asserted-by":"crossref","unstructured":"I. Horrocks, U. Sattler, and S. Tobies. Practical reasoning for very expressive description logics. In Areces et al. [13],pages 239-264.","DOI":"10.1093\/jigpal\/8.3.239"},{"key":"10.1016\/S1570-2464(07)80017-6_bib94","series-title":"Proceedings of the 17th International Conference on Automated Deduction (CADE-17)","first-page":"482","article-title":"Reasoning with individuals for the description logic SHTQ","author":"Horrocks","year":"2000"},{"issue":"1","key":"10.1016\/S1570-2464(07)80017-6_bib95","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1093\/jigpal\/jzk003","article-title":"A minimal hybrid logic for intervals","volume":"14","author":"Hussain","year":"2006","journal-title":"Logic Journal of the IGPL"},{"key":"10.1016\/S1570-2464(07)80017-6_bib96","doi-asserted-by":"crossref","first-page":"227","DOI":"10.1111\/j.1755-2567.1971.tb00071.x","article-title":"Formal properties of \u201cnow\u201d","volume":"37","author":"Kamp","year":"1971","journal-title":"Theoria"},{"key":"10.1016\/S1570-2464(07)80017-6_bib97","doi-asserted-by":"crossref","first-page":"185","DOI":"10.1023\/A:1004952317628","article-title":"A logic for reasoning about relative similarity","volume":"58","author":"Konikowska","year":"1997","journal-title":"Studia Logica"},{"key":"10.1016\/S1570-2464(07)80017-6_bib98","unstructured":"B. Kooi, G. Renardel de Lavalette, and R. Verbrugge. Strong completeness for non-compact hybrid logics. In Schmidt et al. [127], pages 212-223."},{"key":"10.1016\/S1570-2464(07)80017-6_bib99","article-title":"Frame and Labels","author":"Kurtonina","year":"1994"},{"issue":"1","key":"10.1016\/S1570-2464(07)80017-6_bib100","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/j.artint.2004.02.002","article-title":"E-connections of abstract description systems","volume":"156","author":"Kutz","year":"2004","journal-title":"Artificial Intelli-gence"},{"issue":"2","key":"10.1016\/S1570-2464(07)80017-6_bib101","doi-asserted-by":"crossref","first-page":"260","DOI":"10.1145\/635499.635504","article-title":"Logics of metric spaces","volume":"4","author":"Kutz","year":"2003","journal-title":"ACM Transactions onComputational Logic"},{"key":"10.1016\/S1570-2464(07)80017-6_bib102","volume":"volume 57","author":"L\u00e9vy","year":"1965"},{"key":"10.1016\/S1570-2464(07)80017-6_bib103","article-title":"An improved NExpTime-hardness result for the description logic ALC extended with inverse roles, nom-inals, and counting","author":"Lutz","year":"2004"},{"issue":"3","key":"10.1016\/S1570-2464(07)80017-6_bib104","doi-asserted-by":"crossref","first-page":"88","DOI":"10.1145\/122296.122309","article-title":"Inside the LOOM description classifier","volume":"2","author":"MacGregor","year":"1991","journal-title":"SIGART Bulletin"},{"key":"10.1016\/S1570-2464(07)80017-6_bib105","series-title":"Proceedings of the 2002 International Workshop on Description Logics (DL'02)","article-title":"Narcissists, stepmothers and spies","author":"Marx","year":"2002"},{"key":"10.1016\/S1570-2464(07)80017-6_bib106","volume":"volume 4","author":"Marx","year":"1997"},{"key":"10.1016\/S1570-2464(07)80017-6_bib107","unstructured":"D. McGuinness and F. van Harmelen. OWL Web Ontology Language. Overview. http:\/\/www.w3.org\/TR\/ owl-features. Last visited: Dec\/05."},{"key":"10.1016\/S1570-2464(07)80017-6_bib108","doi-asserted-by":"crossref","first-page":"141","DOI":"10.2307\/1969080","article-title":"The algebra of topology","volume":"45","author":"McKinsey","year":"1944","journal-title":"Annals of Mathematics"},{"key":"10.1016\/S1570-2464(07)80017-6_bib109","series-title":"Mind","first-page":"457","article-title":"The unreality of time","author":"McTaggart","year":"1908"},{"key":"10.1016\/S1570-2464(07)80017-6_bib110","unstructured":"M. Mundhenk, T. Schneider, T. Schwentick, and V. Weber. Complexity of hybrid logics over transitive frames. In Schlinglof [126]."},{"key":"10.1016\/S1570-2464(07)80017-6_bib111","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1007\/BF01128202","article-title":"A. N. Prior's rediscovery of tense logic","volume":"39","author":"\u00d8hrstr\u00f8m","year":"1993","journal-title":"Erkenntnis"},{"key":"10.1016\/S1570-2464(07)80017-6_bib112","series-title":"Incomplete Information: Rough Set Analysis","year":"1997"},{"issue":"1","key":"10.1016\/S1570-2464(07)80017-6_bib113","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1016\/0020-0190(85)90127-9","article-title":"PDL with data constants","volume":"20","author":"Passy","year":"1985","journal-title":"Information Processing Letters"},{"key":"10.1016\/S1570-2464(07)80017-6_bib114","first-page":"512","article-title":"Quantifiers in combinatory PDL: completeness, definability, incompleteness","volume":"volume 199","author":"Passy","year":"1985"},{"issue":"2","key":"10.1016\/S1570-2464(07)80017-6_bib115","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1016\/0890-5401(91)90026-X","article-title":"An essay in combinatory dynamic logic","volume":"93","author":"Passy","year":"1991","journal-title":"Information and Computation"},{"key":"10.1016\/S1570-2464(07)80017-6_bib116","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1353\/frc.1958.0008","article-title":"The syntax of time-distinctions","volume":"18","author":"Prior","year":"1958","journal-title":"Franciscan Studies"},{"key":"10.1016\/S1570-2464(07)80017-6_bib117","series-title":"Past, Present and Future","author":"Prior","year":"1967"},{"key":"10.1016\/S1570-2464(07)80017-6_bib118","series-title":"Papers on Time and Tense","author":"Prior","year":"1968"},{"key":"10.1016\/S1570-2464(07)80017-6_bib119","series-title":"Worlds, Times and Selves","article-title":"A feature value logic","author":"Prior","year":"1977"},{"issue":"3","key":"10.1016\/S1570-2464(07)80017-6_bib120","doi-asserted-by":"crossref","first-page":"1011","DOI":"10.2307\/2695091","article-title":"An axiomatization of full computation tree logic","volume":"66","author":"Reynolds","year":"2001","journal-title":"Journal of Symbolic Logic"},{"key":"10.1016\/S1570-2464(07)80017-6_bib121","series-title":"Temporal Representation and Inference","author":"Richards","year":"1989"},{"key":"10.1016\/S1570-2464(07)80017-6_bib122","series-title":"Handbook of Logic and Language","first-page":"475","article-title":"Feature logics","author":"Rounds","year":"1997"},{"key":"10.1016\/S1570-2464(07)80017-6_bib123","doi-asserted-by":"crossref","unstructured":"U. Sattler and M. Vardi. The hybrid \u03bc-calculus. In Gor\u00e9 et al. [81], pages 76-91.","DOI":"10.1007\/3-540-45744-5_7"},{"key":"10.1016\/S1570-2464(07)80017-6_bib124","series-title":"Proceedings of the 12th International Joint Con-ference on Artificial Intelligence (IJCAI'91)","first-page":"466","article-title":"A correspondence theory for terminological logics","author":"Schild","year":"1991"},{"key":"10.1016\/S1570-2464(07)80017-6_bib125","series-title":"Methods for Modalities 4","year":"2005"},{"key":"10.1016\/S1570-2464(07)80017-6_bib126","series-title":"Proceedings of 5th AiML Conference","year":"2004"},{"key":"10.1016\/S1570-2464(07)80017-6_bib127","article-title":"A cut-free sequent calculus for elementary situated reasoning","author":"Seligman","year":"1991"},{"key":"10.1016\/S1570-2464(07)80017-6_bib128","series-title":"Advances in Intensional Logic","first-page":"107","article-title":"The logic of correct description","author":"Seligman","year":"1997"},{"issue":"5","key":"10.1016\/S1570-2464(07)80017-6_bib129","doi-asserted-by":"crossref","first-page":"671","DOI":"10.1093\/logcom\/11.5.671","article-title":"Intemalization: The case of hybrid logics","volume":"ll","author":"Seligman","year":"2001","journal-title":"Journal of Logic and Computation"},{"key":"10.1016\/S1570-2464(07)80017-6_bib130","series-title":"Verifying modal formulae over I\/O-automata by means of type theory Logic group preprint series","author":"Sellink","year":"1994"},{"key":"10.1016\/S1570-2464(07)80017-6_bib131","article-title":"The Proof Theory and Semantics of Intuitionistic Modal Logic","author":"Simpson","year":"1994"},{"key":"10.1016\/S1570-2464(07)80017-6_bib132","article-title":"Complexity of Modal Logics","author":"Spaan","year":"1993"},{"key":"10.1016\/S1570-2464(07)80017-6_bib133","series-title":"Proceedings of ESSLLI'2005 StudentSession","first-page":"342","article-title":"Hybrid definability in topological spaces","author":"Sustretov","year":"2005"},{"issue":"1","key":"10.1016\/S1570-2464(07)80017-6_bib134","doi-asserted-by":"crossref","first-page":"223","DOI":"10.2178\/jsl\/1107298517","article-title":"Interpolation for extended modal languages","volume":"70","author":"ten Cate","year":"2005","journal-title":"Journal of Symbolic Logic"},{"key":"10.1016\/S1570-2464(07)80017-6_bib135","article-title":"Model theory for extended modal languages","author":"ten Cate","year":"2005"},{"key":"10.1016\/S1570-2464(07)80017-6_bib136","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1007\/s10992-005-9012-9","article-title":"Expressivity of second-order propositional modal logic","volume":"35","author":"ten Cate","year":"2006","journal-title":"Journal of Philosophical Logic"},{"issue":"3","key":"10.1016\/S1570-2464(07)80017-6_bib137","doi-asserted-by":"crossref","first-page":"281","DOI":"10.1007\/s10849-005-5787-x","article-title":"Guarded fragments with constants","volume":"14","author":"ten Cate","year":"2005","journal-title":"Journal of Logic, Language andInformation"},{"key":"10.1016\/S1570-2464(07)80017-6_bib138","series-title":"Proceedings of5th AiML Conference, volume 3634 of Lecture Notes in Computer Science","first-page":"339","article-title":"On the complexity of hybrid logics with binders","author":"ten Cate","year":"2005"},{"issue":"3","key":"10.1016\/S1570-2464(07)80017-6_bib139","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1093\/jigpal\/jzi024","article-title":"Hybrid logics with Sahlqvist axioms","volume":"13","author":"ten Cate","year":"2005","journal-title":"Logic Journal of the IGPL"},{"key":"10.1016\/S1570-2464(07)80017-6_bib140","article-title":"Hybrid Languages","author":"Tzakova","year":"1999"},{"key":"10.1016\/S1570-2464(07)80017-6_bib141","first-page":"278","article-title":"Tableaux calculi for hybrid logics","volume":"volume 1617","author":"Tzakova","year":"1999"},{"key":"10.1016\/S1570-2464(07)80017-6_bib142","series-title":"Proceedings of the 25th International Colloquium on Automata, Languages and Programming","first-page":"628","article-title":"Reasoning about the past with two-way automata","author":"Vardi","year":"1998"},{"key":"10.1016\/S1570-2464(07)80017-6_bib143","article-title":"Many-dimensional modal logic","author":"Venema","year":"1991"},{"key":"10.1016\/S1570-2464(07)80017-6_bib144","series-title":"Labelled Non-Classical Logics","author":"Vigan\u00f6","year":"2000"},{"key":"10.1016\/S1570-2464(07)80017-6_bib145","article-title":"Now and Then: a formal study in the logic of tense anaphora","author":"Vlach","year":"1973"}],"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:S1570246407800176?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1570246407800176?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:16:17Z","timestamp":1761606977000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1570246407800176"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007]]},"ISBN":["9780444516909"],"references-count":145,"URL":"https:\/\/doi.org\/10.1016\/s1570-2464(07)80017-6","relation":{},"ISSN":["1570-2464"],"issn-type":[{"value":"1570-2464","type":"print"}],"subject":[],"published":{"date-parts":[[2007]]}}}