A path characterization of validity for multimodal logics

• Main Author: Heilala, Samuli
• Other Authors: Brigitte Pientka (Internal/Supervisor)
• Format: Others
• Language: en
• Published: McGill University 2009
• Subjects: Applied Sciences - Computer Science
• Online Access: http://digitool.Library.McGill.CA:80/R/?func=dbin-jump-full&object_id=66781

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.