Reasoning in Many-Valued Multi-Modal Logic: A Uniform and General Approach

Background: Multi-modal logic has found many applications in computer science, also providing a framework to model temporal and spatial information. Reasoning in this logic is crucial in many real-world applications from different fields. At the same time, these applications live in scenarios characterized by uncertainty and vagueness in the data. Objectives: We aim to introduce a possible many-valued extension for multi-modal logic based on the family of finite FLew-algebras, as well as a sound and complete reasoning system for such logic. Methods: In order to give a general framework for many-valued temporal and spatial logic, we introduce the notion of a many-valued linear order, allowing for the definition of a many-valued semantics of modal frames. The reasoning system is based on the analytic tableau technique and implemented as part of an open-source framework for representing, reasoning, and learning from structured and unstructured data. Results: The performance of the tableau implementation has been addressed through extensive experiments, changing both the underlying logic and algebra and solving both the satisfiability and validity problem for formulas of different complexity. Conclusions: We provide an open-source framework to work with many-valued temporal and spatial logic and a reasoning tool to check satisfiability and validity of formulas from such logic.