Switch to: References

Add citations

You must login to add citations.
  1. Tableau-based decision procedure for the multiagent epistemic logic with all coalitional operators for common and distributed knowledge.M. Ajspur, V. Goranko & D. Shkatov - 2013 - Logic Journal of the IGPL 21 (3):407-437.
    We develop a conceptually clear, intuitive, and feasible decision procedure for testing satisfiability in the full multi\-agent epistemic logic \CMAELCD\ with operators for common and distributed knowledge for all coalitions of agents mentioned in the language. To that end, we introduce Hintikka structures for \CMAELCD\ and prove that satisfiability in such structures is equivalent to satisfiability in standard models. Using that result, we design an incremental tableau-building procedure that eventually constructs a satisfying Hintikka structure for every satisfiable input set of (...)
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  • ExpTime Tableau Decision Procedures for Regular Grammar Logics with Converse.Linh Anh Nguyen & Andrzej Szałas - 2011 - Studia Logica 98 (3):387-428.
    Grammar logics were introduced by Fariñas del Cerro and Penttonen in 1988 and have been widely studied. In this paper we consider regular grammar logics with converse ( REG c logics) and present sound and complete tableau calculi for the general satisfiability problem of REG c logics and the problem of checking consistency of an ABox w.r.t. a TBox in a REG c logic. Using our calculi we develop ExpTime (optimal) tableau decision procedures for the mentioned problems, to which various (...)
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  • Converse-PDL with regular inclusion axioms: a framework for MAS logics.Barbara Dunin-Kęplicz, Linh Anh Nguyen & Andrzej Szalas - 2011 - Journal of Applied Non-Classical Logics 21 (1):61-91.
    In this paper we study automated reasoning in the modal logic CPDLreg which is a combination of CPDL (Propositional Dynamic Logic with Converse) and REGc (Regular Grammar Logic with Converse). The logic CPDL is widely used in many areas, including program verification, theory of action and change, and knowledge representation. On the other hand, the logic REGc is applicable in reasoning about epistemic states and ontologies (via Description Logics). The modal logic CPDLreg can serve as a technical foundation for reasoning (...)
    Download  
     
    Export citation  
     
    Bookmark   1 citation