Paper Info
Title
Decidability of an Xstit Logic
Abstract
This paper presents proofs of completeness and decidability of a non-temporal fragment of an Xstit logic. This shows a distinction between the non-temporal fragments of Xstit logic and regular stit logic since the latter is undecidable. The proof of decidability is via the finite model property. The finite model property is shown to hold by constructing a filtration. However, the set that is used to filter the models isn't simply closed under subformulas, it has more complex closure conditions. The filtration set is akin to the Fischer---Ladner closure of a set used to show completeness and decidability of propositional dynamic logic.
Year
DOI
Venue
2014
10.1007/s11225-013-9492-5
Studia Logica
Keywords
Field
DocType
Stit,Xstit,S5,Decidability,Kripke models
Discrete mathematics,Finite model property,Algorithm,Closure (topology),Decidability,Mathematical proof,Dynamic logic (digital electronics),Completeness (statistics),Intermediate logic,Mathematics,Undecidable problem
Journal
Volume
Issue
ISSN
102
3
0039-3215
Citations 
PageRank 
References 
3
0.45
11
Authors
1
Name
Order
Citations
PageRank
Gillman Payette162.89