Local is Best: Efficient Reductions to Modal Logic K

Papacchini, Fabio ORCID: 0000-0002-0310-7378, Nalon, Claudia, Hustadt, Ullrich ORCID: 0000-0002-0455-0267 and Dixon, Clare ORCID: 0000-0002-4610-9533 (2022) Local is Best: Efficient Reductions to Modal Logic K. JOURNAL OF AUTOMATED REASONING, 66 (4). pp. 639-666.

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

Official URL: http://dx.doi.org/10.1007/s10817-022-09630-6

Abstract

<jats:title>Abstract</jats:title><jats:p>We present novel reductions of extensions of the basic modal logic <jats:inline-formula><jats:alternatives><jats:tex-math>$${\textsf {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 axioms <jats:inline-formula><jats:alternatives><jats:tex-math>$$\textsf {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>$$\textsf {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>$$\textsf {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>$$\textsf {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>$$\textsf {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 Separated Normal Form with Sets of Modal Levels <jats:inline-formula><jats:alternatives><jats:tex-math>$$\textsf {SNF} _{sml}$$</jats:tex-math><mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:msub> <mml:mi>SNF</mml:mi> <mml:mrow> <mml:mi>sml</mml:mi> </mml:mrow> </mml:msub> </mml:math></jats:alternatives></jats:inline-formula>. The reductions typically result in smaller formulae than the reductions by Kracht. The reductions to <jats:inline-formula><jats:alternatives><jats:tex-math>$$\textsf {SNF} _{sml}$$</jats:tex-math><mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:msub> <mml:mi>SNF</mml:mi> <mml:mrow> <mml:mi>sml</mml:mi> </mml:mrow> </mml:msub> </mml:math></jats:alternatives></jats:inline-formula> combined with a reduction to <jats:inline-formula><jats:alternatives><jats:tex-math>$$\textsf {SNF} _{ml}$$</jats:tex-math><mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:msub> <mml:mi>SNF</mml:mi> <mml:mrow> <mml:mi>ml</mml:mi> </mml:mrow> </mml:msub> </mml:math></jats:alternatives></jats:inline-formula> allow us to use the local reasoning of the prover <jats:inline-formula><jats:alternatives><jats:tex-math>$${\text {K}_{\text {S}}}{\text {P}}$$</jats:tex-math><mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:msub> <mml:mtext>K</mml:mtext> <mml:mtext>S</mml:mtext> </mml:msub> <mml:mtext>P</mml:mtext> </mml:mrow> </mml:math></jats:alternatives></jats:inline-formula> to determine the satisfiability of modal formulae in the considered logics. We show experimentally that the combination of our reductions with the prover <jats:inline-formula><jats:alternatives><jats:tex-math>$${\text {K}_{\text {S}}}{\text {P}}$$</jats:tex-math><mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:msub> <mml:mtext>K</mml:mtext> <mml:mtext>S</mml:mtext> </mml:msub> <mml:mtext>P</mml:mtext> </mml:mrow> </mml:math></jats:alternatives></jats:inline-formula> performs well when compared with a specialised resolution calculus for these logics, the built-in reductions of the first-order prover SPASS, and the higher-order logic prover LEO-III.</jats:p>

Item Type:	Article
Uncontrolled Keywords:	Modal logics, Theorem proving, Resolution method
Divisions:	Faculty of Science and Engineering > School of Electrical Engineering, Electronics and Computer Science
Depositing User:	Symplectic Admin
Date Deposited:	07 Jul 2022 10:31
Last Modified:	22 Nov 2023 11:36
DOI:	10.1007/s10817-022-09630-6
Open Access URL:	https://doi.org/10.1007/s10817-022-09630-6
Related URLs:	Author Publisher
URI:	https://livrepository.liverpool.ac.uk/id/eprint/3157936