Document Type

Report

Date

9-1990

Embargo Period

5-1-2012

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.

Additional Information

School of Computer and Information Science, Syracuse University, SU-CIS-90-30

Source

local

Share

COinS
 
 

To view the content in your browser, please download Adobe Reader or, alternately,
you may Download the file to your hard drive.

NOTE: The latest versions of Adobe Reader do not support viewing PDF files within Firefox on Mac OS and if you are using a modern (Intel) Mac, there is no official plugin for viewing PDF files within the browser window.