Local Reductions for the Modal Cube⋆

Claudia Nalon; Ullrich Hustadt; Fabio Papacchini; Clare Dixon

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

Local Reductions for the Modal Cube⋆

Claudia Nalon, Ullrich Hustadt, Fabio Papacchini, Clare Dixon

Autonomy and Verification

Research output: Chapter in Book/Conference proceeding › Conference contribution › 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 KSP. 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	Automated Reasoning - 11th International Joint Conference, IJCAR 2022, Proceedings
Editors	Jasmin Blanchette, Laura Kovács, Dirk Pattinson
Pages	486-505
Number of pages	20
DOIs	https://doi.org/10.1007/978-3-031-10769-6_29
Publication status	Published - 1 Aug 2022

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	13385
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Access to Document

10.1007/978-3-031-10769-6_29Licence: CC BY

Novel Locomotion for Extreme Environments (Space)
Smith, K. (PI), Parslew, B. (CoI) & Weightman, A. (CoI)
16/03/20 → 31/03/21
Project: Research
Robotics and Artificial Intelligence for Nuclear (RAIN)
Lennox, B. (PI), Arvin, F. (CoI), Brown, G. (CoI), Carrasco Gomez, J. (CoI), Da Via, C. (CoI), Furber, S. (CoI), Luján, M. (CoI), Watson, S. (CoI), Watts, S. (CoI) & Weightman, A. (CoI)
2/10/17 → 31/03/22
Project: Research

Cite this

@inproceedings{eb6f9649a9c84bd1bf97080b5fe3ad84,

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 KSP. We define benchmarks for these logics and experiment with thereduction approach as compared to an existing resolution calculus withspecialised inference rules for the various logics.",

author = "Claudia Nalon and Ullrich Hustadt and Fabio Papacchini and Clare Dixon",

note = "Funding Information: 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). Publisher Copyright: {\textcopyright} 2022, The Author(s).",

year = "2022",

month = aug,

day = "1",

doi = "10.1007/978-3-031-10769-6_29",

language = "English",

series = "Lecture Notes in Computer Science ",

publisher = "Springer",

pages = "486--505",

editor = "Jasmin Blanchette and Laura Kov{\'a}cs and Dirk Pattinson",

booktitle = "Automated Reasoning - 11th International Joint Conference, IJCAR 2022, Proceedings",

}

Local Reductions for the Modal Cube⋆. / Nalon, Claudia; Hustadt, Ullrich; Papacchini, Fabio et al.
Automated Reasoning - 11th International Joint Conference, IJCAR 2022, Proceedings. ed. / Jasmin Blanchette; Laura Kovács; Dirk Pattinson. 2022. p. 486-505 (Lecture Notes in Computer Science ; Vol. 13385).

Research output: Chapter in Book/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Local Reductions for the Modal Cube⋆

AU - Nalon, Claudia

AU - Hustadt, Ullrich

AU - Papacchini, Fabio

AU - Dixon, Clare

N1 - Funding Information: 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). Publisher Copyright: © 2022, The Author(s).

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 KSP. We define benchmarks for these logics and experiment with thereduction approach as compared to an existing resolution calculus withspecialised 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 KSP. We define benchmarks for these logics and experiment with thereduction approach as compared to an existing resolution calculus withspecialised inference rules for the various logics.

U2 - 10.1007/978-3-031-10769-6_29

DO - 10.1007/978-3-031-10769-6_29

M3 - Conference contribution

T3 - Lecture Notes in Computer Science

SP - 486

EP - 505

BT - Automated Reasoning - 11th International Joint Conference, IJCAR 2022, Proceedings

A2 - Blanchette, Jasmin

A2 - Kovács, Laura

A2 - Pattinson, Dirk

ER -

Local Reductions for the Modal Cube⋆

Abstract

Publication series

Access to Document

Fingerprint

Projects

Novel Locomotion for Extreme Environments (Space)

Robotics and Artificial Intelligence for Nuclear (RAIN)

Cite this