Document Type
Report
Date
9-1990
Keywords
logic
Language
English
Disciplines
Computer Sciences
Description/Abstract
Modal formulas can be proved by translating them into a three-typed logic and then using unification and resolution, with axioms describing properties of the reachability relation among possible worlds. In this paper, we improve on the algorithms in [1], showing that "strong skolemisation" and occurrence checks are not needed for proving theorems of Q, T, Q4, and S4. We also extend the 'path logic' approach to S5, give the appropriate unification algorithm, and prove its correctness.
Recommended Citation
Zhang, Xiaolin and Mohan, Chilukuri K., "Unification in Modal Theorem Proving" (1990). Electrical Engineering and Computer Science - Technical Reports. 87.
https://surface.syr.edu/eecs_techreports/87
Source
local
Additional Information
School of Computer and Information Science, Syracuse University, SU-CIS-90-30