Efficient Local Reductions to Basic Modal Logic



Papacchini, Fabio ORCID: 0000-0002-0310-7378, Nalon, Claudia, Hustadt, Ullrich ORCID: 0000-0002-0455-0267 and Dixon, Clare ORCID: 0000-0002-4610-9533
(2021) Efficient Local Reductions to Basic Modal Logic. In: Automated Deduction – CADE 28. Lecture Notes in Computer Science, 12699 . Springer International Publishing, pp. 76-92. ISBN 978-3-030-79875-8

[img] Text
cade2021.pdf - Author Accepted Manuscript

Download (401kB) | Preview

Abstract

<jats:title>Abstract</jats:title><jats:p>We present novel reductions of the propositional modal logics "Image missing"<!-- image only, no MathML or LaTex --> , "Image missing"<!-- image only, no MathML or LaTex --> , "Image missing"<!-- image only, no MathML or LaTex --> , "Image missing"<!-- image only, no MathML or LaTex --> and "Image missing"<!-- image only, no MathML or LaTex --> to Separated Normal Form with Sets of Modal Levels. The reductions result in smaller formulae than the well-known reductions by Kracht and allow us to use the local reasoning of the prover "Image missing"<!-- image only, no MathML or LaTex --> to determine the satisfiability of modal formulae in these logics. We show experimentally that the combination of our reductions with the prover "Image missing"<!-- image only, no MathML or LaTex --> performs well when compared with a specialised resolution calculus for these logics and with the b̆uilt-in reductions of the first-order prover SPASS.</jats:p>

Item Type: Book Section
Divisions: Faculty of Science and Engineering > School of Electrical Engineering, Electronics and Computer Science
Depositing User: Symplectic Admin
Date Deposited: 02 Aug 2021 10:51
Last Modified: 18 Jan 2023 21:35
DOI: 10.1007/978-3-030-79876-5_5
Related URLs:
URI: https://livrepository.liverpool.ac.uk/id/eprint/3131113