A tableau for Many-Valued Multi-Modal Logic
Date:
Melvin Fitting proposed in 1995 a tableau for many-valued modal logic, where the many-valued component was addressed leveraging Heyting algebras. However, the latter are not suitable to model common fuzzy logics different from Gödel logic, such as the widespread Łukasiewicz logic. We introduce a generalization of Fitting’s many-valued modal logic based on the more general FLew-algebras, encompassing both Heyting algebras and all popular fuzzy logics. Moreover, we propose a tableau system to address the satisfiability of formulae in the given framework, also allowing for the definition of more modalities, hence enabling for the treatment of common temporal and spatial modal logics, among others. The system has also been implemented in the Julia programming language as part of an open-source framework for symbolic learning and reasoning, namely Sole.jl.