Local Reductions for the Modal Cube


Nalon, Claudia, Hustadt, Ullrich ORCID: 0000-0002-0455-0267, Papacchini, Fabio ORCID: 0000-0002-0310-7378 and Dixon, Clare ORCID: 0000-0002-4610-9533 (2022) Local Reductions for the Modal Cube. In: Automated Reasoning. Lecture Notes in Computer Science, 13385 . Springer International Publishing, pp. 486-505. ISBN 978-3-031-10768-9

Access the full-text of this item by clicking on the Open Access link.

Abstract

<jats:title>Abstract</jats:title><jats:p>The modal logic<jats:inline-formula><jats:alternatives><jats:tex-math>$${\mathsf {K}}$$</jats:tex-math><mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"><mml:mi>K</mml:mi></mml:math></jats:alternatives></jats:inline-formula>is commonly used to represent and reason about necessity and possibility and its extensions with combinations of additional axioms are used to represent knowledge, belief, desires and intentions. Here we present local reductions of all propositional modal logics in the so-called modal cube, that is, extensions of<jats:inline-formula><jats:alternatives><jats:tex-math>$${\mathsf {K}}$$</jats:tex-math><mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"><mml:mi>K</mml:mi></mml:math></jats:alternatives></jats:inline-formula>with arbitrary combinations of the axioms<jats:inline-formula><jats:alternatives><jats:tex-math>$${\mathsf {B}}$$</jats:tex-math><mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"><mml:mi>B</mml:mi></mml:math></jats:alternatives></jats:inline-formula>,<jats:inline-formula><jats:alternatives><jats:tex-math>$${\mathsf {D}}$$</jats:tex-math><mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"><mml:mi>D</mml:mi></mml:math></jats:alternatives></jats:inline-formula>,<jats:inline-formula><jats:alternatives><jats:tex-math>$${\mathsf {T}}$$</jats:tex-math><mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"><mml:mi>T</mml:mi></mml:math></jats:alternatives></jats:inline-formula>,<jats:inline-formula><jats:alternatives><jats:tex-math>$${\mathsf {4}}$$</jats:tex-math><mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"><mml:mn>4</mml:mn></mml:math></jats:alternatives></jats:inline-formula>and<jats:inline-formula><jats:alternatives><jats:tex-math>$${\mathsf {5}}$$</jats:tex-math><mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"><mml:mn>5</mml:mn></mml:math></jats:alternatives></jats:inline-formula>to a normal form comprising a formula and the set of modal levels it occurs at. Using these reductions we can carry out reasoning for all these logics with the theorem prover "Image missing"<!-- image only, no MathML or LaTex -->. We define benchmarks for these logics and experiment with the reduction approach as compared to an existing resolution calculus with specialised inference rules for the various logics.</jats:p>

Item Type: Book Section
Depositing User: Symplectic Admin
Date Deposited: 03 Oct 2022 08:14
Last Modified: 27 Nov 2023 03:19
DOI: 10.1007/978-3-031-10769-6_29
Open Access URL: https://doi.org/10.1007/978-3-031-10769-6_29
Related URLs:
URI: https://livrepository.liverpool.ac.uk/id/eprint/3164984
Dimensions
Altmetric
CORE (COnnecting REpositories)