The realization of the hybrid multi-modal logic theorem prover in the term rewriting system CafeOBJ. (English) Zbl 0935.03020
CafeOBJ is a term rewriting system which is based on equational logic. Using CafeOBJ, this report aims to study the possibility of realization of the method of M. Finger and D. Gabbay [see D. M. Gabbay, I. Hodkinson and M. Reynolds, Temporal logic. Vol. 1. Mathematical foundations and computational aspects (Oxford Logic Guides 28) (Clarendon Press, Oxford) (1994; Zbl 0921.03023), Chapter 14: Adding a temporal dimension to a logic system], and gives a concrete automated theorem-prover for some modal logics (S4 and S5). We will adopt the Beth tableau proof as the basis of the automated theorem-prover.
MSC:
03B35 | Mechanization of proofs and logical operations |
03B45 | Modal logic (including the logic of norms) |
68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |
68Q42 | Grammars and rewriting systems |