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