Home > Research > Publications & Outputs > Local is Best: Efficient Reductions to Modal Lo...

Research

Associated organisational units

Links

Text available via DOI:

Keywords

View graph of relations

Local is Best: Efficient Reductions to Modal Logic K

Research output: Contribution to Journal/Magazine › Journal article › peer-review

Published

Standard

Local is Best: Efficient Reductions to Modal Logic K. / Papacchini, Fabio; Nalon, Cláudia; Hustadt, Ullrich et al.
In: Journal of Automated Reasoning, Vol. 66, No. 4, 4, 23.05.2022, p. 639-666.

Research output: Contribution to Journal/Magazine › Journal article › peer-review

Harvard

Papacchini, F, Nalon, C, Hustadt, U & Dixon, C 2022, 'Local is Best: Efficient Reductions to Modal Logic K', Journal of Automated Reasoning, vol. 66, no. 4, 4, pp. 639-666. https://doi.org/10.1007/s10817-022-09630-6

APA

Papacchini, F., Nalon, C., Hustadt, U., & Dixon, C. (2022). Local is Best: Efficient Reductions to Modal Logic K. Journal of Automated Reasoning, 66(4), 639-666. Article 4. https://doi.org/10.1007/s10817-022-09630-6

Vancouver

Papacchini F, Nalon C, Hustadt U, Dixon C. Local is Best: Efficient Reductions to Modal Logic K. Journal of Automated Reasoning. 2022 May 23;66(4):639-666. 4. doi: 10.1007/s10817-022-09630-6

Author

Papacchini, Fabio ; Nalon, Cláudia ; Hustadt, Ullrich et al. / Local is Best: Efficient Reductions to Modal Logic K. In: Journal of Automated Reasoning. 2022 ; Vol. 66, No. 4. pp. 639-666.

Bibtex

@article{d24b889700604398ad995f751bfdd452,
title = "Local is Best: Efficient Reductions to Modal Logic K",
abstract = "We present novel reductions of extensions of the basic modal logic K with axioms B, D, T, 4 and 5 to Separated Normal Form with Sets of Modal Levels SNFsml. The reductions typically result in smaller formulae than the reductions by Kracht. The reductions to SNFsml combined with a reduction to SNFml allow us to use the local reasoning of the prover KSP to determine the satisfiability of modal formulae in the considered logics. We show experimentally that the combination of our reductions with the prover KSP 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.",
keywords = "Article, Modal logics, Theorem proving, Resolution method",
author = "Fabio Papacchini and Cl{\'a}udia Nalon and Ullrich Hustadt and Clare Dixon",
year = "2022",
month = may,
day = "23",
doi = "10.1007/s10817-022-09630-6",
language = "English",
volume = "66",
pages = "639--666",
journal = "Journal of Automated Reasoning",
issn = "0168-7433",
publisher = "Springer Netherlands",
number = "4",

}

RIS

TY - JOUR

T1 - Local is Best: Efficient Reductions to Modal Logic K

AU - Papacchini, Fabio

AU - Nalon, Cláudia

AU - Hustadt, Ullrich

AU - Dixon, Clare

PY - 2022/5/23

Y1 - 2022/5/23

N2 - We present novel reductions of extensions of the basic modal logic K with axioms B, D, T, 4 and 5 to Separated Normal Form with Sets of Modal Levels SNFsml. The reductions typically result in smaller formulae than the reductions by Kracht. The reductions to SNFsml combined with a reduction to SNFml allow us to use the local reasoning of the prover KSP to determine the satisfiability of modal formulae in the considered logics. We show experimentally that the combination of our reductions with the prover KSP 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.

AB - We present novel reductions of extensions of the basic modal logic K with axioms B, D, T, 4 and 5 to Separated Normal Form with Sets of Modal Levels SNFsml. The reductions typically result in smaller formulae than the reductions by Kracht. The reductions to SNFsml combined with a reduction to SNFml allow us to use the local reasoning of the prover KSP to determine the satisfiability of modal formulae in the considered logics. We show experimentally that the combination of our reductions with the prover KSP 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.

KW - Article

KW - Modal logics

KW - Theorem proving

KW - Resolution method

U2 - 10.1007/s10817-022-09630-6

DO - 10.1007/s10817-022-09630-6

M3 - Journal article

VL - 66

SP - 639

EP - 666

JO - Journal of Automated Reasoning

JF - Journal of Automated Reasoning

SN - 0168-7433

IS - 4

M1 - 4

ER -