Local Reductions for the Modal Cube

C. Nalon; U. Hustadt; F. Papacchini; C. Dixon

doi:10.1007/978-3-031-10769-6_29

Local Reductions for the Modal Cube

C. Nalon
, U. Hustadt
, F. Papacchini
, C. Dixon

Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSN › Conference contribution/Paper › peer-review

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.

Original language	English
Title of host publication	International Joint Conference on Automated Reasoning
Editors	Jasmin Blanchette, Laura Kovács, Dirk Pattinson
Pages	486-505
Number of pages	20
Volume	13385
DOIs	https://doi.org/10.1007/978-3-031-10769-6_29
Publication status	Published - 1/08/2022

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	13385 LNAI
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

User-defined Keywords

Formal logic
% reductions
Inference rules
Modal logic
Normal form
Theorem provers
Calculations

Access to Document

10.1007/978-3-031-10769-6_29Licence: CC BY: Creative Commons Attribution 4.0 International License

https://link.springer.com/content/pdf/10.1007/978-3-031-10769-6_29.pdfLicence: CC BY: Creative Commons Attribution 4.0 International License

RAIN Extension Stream B
Joyce, M. (Principal Investigator)
Engineering and Physical Sciences Research Council
1/04/21 → 31/03/22
Project: Research

Cite this

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_29

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)).

@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",

}

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_29

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

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 -

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