Paper Info
Title
Resolution Method for Modal Logic with Well-Founded Frames
Abstract
The modal logic KW with finite temporal frames (i.e. well-founded frames) can be used for verifying the properties where system termination is assumed, such as partial correctness of a system. This paper presents an unification-based proof method for the modal logic KW. In order to certify that a formula does not have a model of a well-founded frame, it is necessary to examine the fact if it has a model, then the model contains infinite transitions. It is, however, difficult to examine with unification-based proof methods. This paper introduces the concept of non-iterative frames. The satisfiability of a formula in noniterative frames agrees with the one in well-founded frames. The size of the evidence of the fact that a formula does not have a model of non-iterative frame is finite. Based on this property, we have constructed a unification-based prover to check unsatisfiability of a formula in KW.
Year
DOI
Venue
1999
10.1007/3-540-48168-0_20
CSL
Keywords
Field
DocType
well-founded frame,modal logic,non-iterative frame,well-founded frames,resolution method,modal logic kw,finite temporal frame,unification-based prover,infinite transition,noniterative frame,unification-based proof method,system termination,satisfiability
Intuitionistic logic,Discrete mathematics,Computer science,Unification,Satisfiability,Correctness,Modal logic,Gas meter prover
Conference
Volume
ISSN
ISBN
1683
0302-9743
3-540-66536-6
Citations 
PageRank 
References 
0
0.34
9
Authors
2
Name
Order
Citations
PageRank
Shigeki Hagihara17812.33
Naoki Yonezaki210720.02