Session S24 - Symbolic Computation: Theory, Algorithms and Applications

No date set.

Guacarí Modal automatic demonstrator for $K$ and $S2$

Luz Amparo Carranza Guerrero

Fundación Universitaria Konrad Lorenz, Colombia   -   This email address is being protected from spambots. You need JavaScript enabled to view it.

\small Modal logic is an extension of classical logic in which modal operators such as $\square$ for necessity and $\lozenge$ for possibility have been introduced. In 1912 C. I. Lewis defined a new conditional called strict implication; this is defined in terms of the material conditional and the notion of necessity $\square(p\rightarrow q)$. The combinations of the axioms proposed by Lewis provided different normal logics, among which \textit{K, T, B, S4} and \textit{S5} are the most used ones.\\

Non-normal logics, also known as Lewis \textit{S1, S2} and \textit{S3} systems, as well as some of their extensions, \textit{S6, S7, S8} and \textit{S9}, share the characteristics of having non-normal worlds, i.e. worlds lacking formulas with the operator of necessity. These extensions were presented in 1943 by Alban, who extends \textit{S2} with the axiom $\lozenge \lozenge p$. In 1963 and 1965 Saul Kripke published ``Semantical Analysis of Modal Logic'', ``Semantical Analysis of Modal Logic II: Non-Normal Propositional Calculi'', which provided a basic tool for semantical analysis of modal logic and non-normal modal systems.\\

From Kripke's semantical perspective, an effective but not very dynamic method is presented for different\-iang valid and invalid formulas based on Beth's analytical tableaux. The analytical tableaux have been widely used in the calculus of non classical logics, because they facilitate the carrying out of proofs and they have favorable algorithmic and semantical features. Non-normal logics are semantically character\-ized by admitting non-normal worlds in their models, i.e. worlds in which the usual semantical conditions for modal operators are not valid.\\

This paper presents the algorithm for the calculus of tableaux for the \textit{K} and \textit{S2} logics, with characterization of non-normal worlds using the Smullyan tree method. In addition, the Guacarí Modal algorithm will be shown. This automatic demonstrator provides users with a demonstration of the evaluated formula or a refutation of the formula in the above-mentioned systems.

Joint work with Luz Amparo Carranza G, Juan Camilo Acosta, (Fundación Universitaria Konrad Lorenz).

View abstract PDF