Standard
Local Reductions for the Modal Cube. / Nalon, C.; Hustadt, U.
; Papacchini, F. et al.
International Joint Conference on Automated Reasoning. ed. / Jasmin Blanchette; Laura Kovács; Dirk Pattinson. Vol. 13385 2022. p. 486-505 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 13385 LNAI).
Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSN › Conference contribution/Paper › peer-review
Harvard
Nalon, C, Hustadt, U
, Papacchini, F & Dixon, C 2022,
Local Reductions for the Modal Cube. in J Blanchette, L Kovács & D Pattinson (eds),
International Joint Conference on Automated Reasoning. vol. 13385, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 13385 LNAI, pp. 486-505.
https://doi.org/10.1007/978-3-031-10769-6_29APA
Nalon, C., Hustadt, U.
, Papacchini, F., & Dixon, C. (2022).
Local Reductions for the Modal Cube. In J. Blanchette, L. Kovács, & D. Pattinson (Eds.),
International Joint Conference on Automated Reasoning (Vol. 13385, pp. 486-505). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 13385 LNAI).
https://doi.org/10.1007/978-3-031-10769-6_29Vancouver
Nalon C, Hustadt U
, Papacchini F, Dixon C.
Local Reductions for the Modal Cube. In Blanchette J, Kovács L, Pattinson D, editors, International Joint Conference on Automated Reasoning. Vol. 13385. 2022. p. 486-505. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-031-10769-6_29
Author
Nalon, C. ; Hustadt, U.
; Papacchini, F. et al. /
Local Reductions for the Modal Cube. International Joint Conference on Automated Reasoning. editor / Jasmin Blanchette ; Laura Kovács ; Dirk Pattinson. Vol. 13385 2022. pp. 486-505 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
Bibtex
@inproceedings{6238d22c7c3a43eba10f22c2286ded02,
title = "Local Reductions for the Modal Cube",
abstract = "The modal logic K 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 K with arbitrary combinations of the axioms B, D, T, 4 and 5 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. 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.",
keywords = "Formal logic, % reductions, Inference rules, Modal logic, Normal form, Theorem provers, Calculations",
author = "C. Nalon and U. Hustadt and F. Papacchini and C. Dixon",
note = "Export Date: 5 September 2022 Funding details: Engineering and Physical Sciences Research Council, EPSRC, EP/N007565/1, EP/R026084/1, EP/R026092/1 Funding text 1: C. Dixon was partially supported by the EPSRC funded RAI Hubs FAIR-SPACE (EP/R026092/1) and RAIN (EP/R026084/1), and the EPSRC funded programme Grant S4 (EP/N007565/1).",
year = "2022",
month = aug,
day = "1",
doi = "10.1007/978-3-031-10769-6_29",
language = "English",
isbn = "9783031107689",
volume = "13385",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "486--505",
editor = "Jasmin Blanchette and Laura Kov{\'a}cs and Dirk Pattinson",
booktitle = "International Joint Conference on Automated Reasoning",
}
RIS
TY - GEN
T1 - Local Reductions for the Modal Cube
AU - Nalon, C.
AU - Hustadt, U.
AU - Papacchini, F.
AU - Dixon, C.
N1 - Export Date: 5 September 2022
Funding details: Engineering and Physical Sciences Research Council, EPSRC, EP/N007565/1, EP/R026084/1, EP/R026092/1
Funding text 1: C. Dixon was partially supported by the EPSRC funded RAI Hubs FAIR-SPACE (EP/R026092/1) and RAIN (EP/R026084/1), and the EPSRC funded programme Grant S4 (EP/N007565/1).
PY - 2022/8/1
Y1 - 2022/8/1
N2 - The modal logic K 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 K with arbitrary combinations of the axioms B, D, T, 4 and 5 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. 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.
AB - The modal logic K 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 K with arbitrary combinations of the axioms B, D, T, 4 and 5 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. 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.
KW - Formal logic
KW - % reductions
KW - Inference rules
KW - Modal logic
KW - Normal form
KW - Theorem provers
KW - Calculations
U2 - 10.1007/978-3-031-10769-6_29
DO - 10.1007/978-3-031-10769-6_29
M3 - Conference contribution/Paper
SN - 9783031107689
VL - 13385
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 486
EP - 505
BT - International Joint Conference on Automated Reasoning
A2 - Blanchette, Jasmin
A2 - Kovács, Laura
A2 - Pattinson, Dirk
ER -
