Modal logics were formalized in the early to mid-20th century to pin down the notion of truth qualified by modalities such as "necessity", "possibility", and "belief", which arise in philosophy and natural languages. They have since outgrown their philosophical trappings and have found applications in type systems and as description languages in many domains of computer science and artificial intelligence. Although they frequently exhibit redundancies in their proof spaces, analytic tableau systems in the style of Smullyan have emerged as popular proof formalisms for modal logics. Inspired by previous work on matrix characterizations by Bibel, Andrews, and Wallen, we propose a new characterization of validity for a family of multimodal logics with interacting accessibility relations which avoids the redundancies common in tableau systems. Our goal is not to produce a high-performance theorem prover for multimodal logics, but to present a fresh way of understanding and establishing multimodal logical validity. / Les logiques modales ont été formalisées vers le milieu du 20ième siècle avec le but de comprendre la notion de vérité qualifiée par des modes tels que "la nécessité", "la possibilité", et "la croyance", qui proviennent de la philosophie et des langages naturels. Ces modes, depuis évolués au-delà de leurs origines philosophiques, trouvent plusieurs applications dans la sémantique statique des langages de programmation et chez les logiques de description de plusieurs domaines de l'informatique et de l'intelligence artificielle. Bien que leurs espaces démonstrationnels présentent des redondances, les systèmes de tableaux analytiques sont un formalisme de démonstration populaire. Nous proposons une nouvelle caractérisation de validité pour une famille de logiques multimodales définies avec des relations d'accessibilité interagissantes qui évite les redondances présentes chez les systèmes de tableaux. Nos innovations sont inspirées par les caractérisations matricielles présentées auparavant par Bibel, Andrews, et Wallen. Notre but n'est pas de produire un démonstrateur automatique de théorèmes de haute performance, mais de présenter une façon originale de comprendre et concevoir la validité logique multimodale.
| Identifer | oai:union.ndltd.org:LACETR/oai:collectionscanada.gc.ca:QMM.66781 |
| Date | January 2009 |
| Creators | Heilala, Samuli |
| Contributors | Brigitte Pientka (Internal/Supervisor) |
| Publisher | McGill University |
| Source Sets | Library and Archives Canada ETDs Repository / Centre d'archives des thèses électroniques de Bibliothèque et Archives Canada |
| Language | English |
| Detected Language | French |
| Type | Electronic Thesis or Dissertation |
| Format | application/pdf |
| Coverage | Master of Science (School of Computer Science) |
| Rights | All items in eScholarship@McGill are protected by copyright with all rights reserved unless otherwise indicated. |
| Relation | Electronically-submitted theses. |
Page generated in 0.0014 seconds