Proceedings of the 2017 5th International Conference on Machinery, Materials and Computing Technology (ICMMCT 2017)

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

Authors
Shigeki Hagihara, Masahiko Tomoishi, Masaya Shimakawa, Naoki Yonezaki
Corresponding Author
Shigeki Hagihara
Available Online April 2017.
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)

Volume Title
Proceedings of the 2017 5th International Conference on Machinery, Materials and Computing Technology (ICMMCT 2017)
Series
Advances in Engineering Research
Publication Date
April 2017
ISBN
978-94-6252-318-0
ISSN
2352-5401
DOI
10.2991/icmmct-17.2017.140How to use a DOI?
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/).

Cite this article

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  -