Combining Unification and Rewriting in Proofs for Modal Logics with First-order Undefinable Frames

DOI

10.2991/icmmct-17.2017.140How to use a DOI?

Keywords

Modal logic; Proof method; Unification; Rewriting

Abstract

We provide a unification-based resolution method for basic modal logics. Because we use a clausal normal form that is quite similar to that in first-order logic, our method has good prospects for importing proof strategies for resolution methods from first-order logic. Furthermore, we show a solution for obtaining a resolution method for the modal logic KM, the frames of which are first-order and undefinable. It is impossible to make a unification rule for the modal logics of first-order undefinable frames in a similar way to that of basic modal logics. In this paper, we use a clausal rewriting rule for KM in addition to modal unification. We expect that this kind of adaptation can be applied to the construction of unification-based proof methods for other modal logics with first-order undefinable frames.

Copyright

© 2017, the Authors. Published by Atlantis Press.

Open Access

This is an open access article distributed under the CC BY-NC license (http://creativecommons.org/licenses/by-nc/4.0/).

Download article (PDF)

TY  - CONF
AU  - Shigeki Hagihara
AU  - Masahiko Tomoishi
AU  - Masaya Shimakawa
AU  - Naoki Yonezaki
PY  - 2017/04
DA  - 2017/04
TI  - Combining Unification and Rewriting in Proofs for Modal Logics with First-order Undefinable Frames
BT  - Proceedings of the 2017 5th International Conference on Machinery, Materials and Computing Technology (ICMMCT 2017)
PB  - Atlantis Press
SP  - 676
EP  - 683
SN  - 2352-5401
UR  - https://doi.org/10.2991/icmmct-17.2017.140
DO  - 10.2991/icmmct-17.2017.140
ID  - Hagihara2017/04
ER  -