Sciweavers

Share
APAL
2010

Logic for update products and steps into the past

9 years 7 months ago
Logic for update products and steps into the past
This paper provides a sound and complete proof system for a language Le+Y that adds to Dynamic Epistemic Logic (DEL) a discrete previous-time operator as well as single symbol formulas that partially reveal the most recent event that occured. The completeness theorem is by filtration followed by model unravelling and other model transformations. Decidability follows from the completeness proof. The degree to which it is important to include the additional single symbol formulas is addressed in a discussion about the difficulties of the completeness for a language LY that only adds the previous-time operator to DEL. Discussion is also given regarding the completeness for a language obtained by removing common knowledge operators from Le+Y .
Joshua Sack
Added 08 Dec 2010
Updated 08 Dec 2010
Type Journal
Year 2010
Where APAL
Authors Joshua Sack
Comments (0)
books