Hybrid logics with paraconsistency

Abstract

The use of hybrid logics allows us to describe relational structures, as they resort to a mechanism to name states, which makes it possible to specify equalities between states, what happens at particular states, and report the presence and absence of transitions between states. Nonetheless, in cases where the information obtained about one of these structures contains contradictions, classical hybrid logic is not enough and a paraconsistent version is necessary to keep it possible to reason within that structure. Paraconsistent logics allow inconsistencies without producing the collapse of the systems and their development has been driven not only by theoretical interest, but also by genuine problems in di erent scienti c domains, such as Computer Science, Medicine or Robotics. The aim of this thesis is the development of paraconsistent hybrid tools that can cope with inconsistencies at the level of the propositional variables, thus locally at each state, and that later can cope with inconsistencies at the level of the accessibility relations as well. We will make it possible to describe inconsistent structures by means of simple hybrid formulas, via diagrams, and we will also present sound and complete tableau-based decision procedures that work even when a database and/or a query are inconsistent. We introduce measures of inconsistency to allow us to compare between di erent structures and sources of information and decide which is less inconsistent and we also de ne new notions of bisimulation.

O uso de lógicas híbridas permite-nos descrever estruturas relacionais, uma vez que recorrem a um mecanismo para nomear estados, o que faz com que seja possível especi ficar igualdades entre estados, o que acontece num estado em particular, e reportar acerca da presença e ausência de transições entre estados. No entanto, em casos em que a informação obtida acerca de uma destas estruturas contém contradições, a lógica híbrida clássica não é sufi ciente e uma versão paraconsistente é necessária de modo a ser possível continuar a fazer inferências em tal estrutura. As lógicas paraconsistentes permitem a ocurrência de inconsistências sem que o sistema colapse, e o seu desenvolvimento tem sido motivado não só por interesses teóricos mas também pelo surgimento de problemas em diferentes domínios científicos, como Ciência da Computação, Medicina ou Robótica. O objetivo desta tese é o desenvolvimento de lóogicas híbridas paraconsistentes capazes de lidar com inconsistências locais ao nível de variáveis proposicionais, e posteriormente capazes também de lidar com inconsistências ao nível das relações de acessibilidade. Vamos tornar possível descrever estruturas inconsistentes através do uso de fórmulas híbridas simples, recorrendo a diagramas, e vamos também apresentar sistemas corretos e completos baseados em tableaux, completamente funcionais mesmo nos casos em que a base de dados e a fórmula cuja consequência queremos estudar são inconsistentes. Introduzimos medidas de inconsistência que nos permitem comparar diferentes estruturas e fontes de informação e decidir qual é menos inconsistente e definimos novas noções de bissimulação.