Switch to: References

Add citations

You must login to add citations.
  1. Tableaux-Based Decision Method for Single-Agent Linear Time Synchronous Temporal Epistemic Logics with Interacting Time and Knowledge.Mai Ajspur & Valentin Goranko - 2013 - In Kamal Lodaya (ed.), Logic and its Applications. Springer. pp. 80--96.
    Temporal epistemic logics are known, from results of Halpern and Vardi, to have a wide range of complexities of the satisfiability problem: from PSPACE, through non-elementary, to highly undecidable. These complexities depend on the choice of some key parameters specifying, inter alia, possible interactions between time and knowledge, such as synchrony and agents' abilities for learning and recall. In this work we develop practically implementable tableau-based decision procedures for deciding satisfiability in single-agent synchronous temporal-epistemic logics with interactions between time and (...)
    Direct download (2 more)  
    Export citation  
  • A General Tableau Method for Propositional Interval Temporal Logics: Theory and Implementation.V. Goranko, A. Montanari, P. Sala & G. Sciavicco - 2006 - Journal of Applied Logic 4 (3):305-330.
    In this paper we focus our attention on tableau methods for propositional interval temporal logics. These logics provide a natural framework for representing and reasoning about temporal properties in several areas of computer science. However, while various tableau methods have been developed for linear and branching time point-based temporal logics, not much work has been done on tableau methods for interval-based ones. We develop a general tableau method for Venema's \cdt\ logic interpreted over partial orders (\nsbcdt\ for short). It combines (...)
    Direct download (3 more)  
    Export citation  
    Bookmark   4 citations  
  • Non-Primitive Recursive Decidability of Products of Modal Logics with Expanding Domains.David Gabelaia, Agi Kurucz, Frank Wolter & Michael Zakharyaschev - 2006 - Annals of Pure and Applied Logic 142 (1):245-268.
    We show that—unlike products of ‘transitive’ modal logics which are usually undecidable—their ‘expanding domain’ relativisations can be decidable, though not in primitive recursive time. In particular, we prove the decidability and the finite expanding product model property of bimodal logics interpreted in two-dimensional structures where one component—call it the ‘flow of time’—is • a finite linear order or a finite transitive tree and the other is composed of structures like • transitive trees/partial orders/quasi-orders/linear orders or only finite such structures expanding (...)
    Direct download (4 more)  
    Export citation  
    Bookmark   5 citations  
  • Tableaux for Logics of Time and Knowledge with Interactions Relating to Synchrony.Clare Dixon, Cláudia Nalon & Michael Fisher - 2004 - Journal of Applied Non-Classical Logics 14 (4):397-445.
    The paper describes tableaux based proof methods for temporal logics of knowledge allowing non-trivial interaction axioms between the modal and temporal components, namely those of synchrony and no learning and synchrony and perfect recall. The interaction axioms allow the description of how knowledge evolves over time and makes reasoning in such logics theoretically more complex. Such logics can be used to specify systems that involve the knowledge of processes or agents and which change over time, for example agent based systems, (...)
    Direct download (3 more)  
    Export citation  
    Bookmark   2 citations