Switch to: References

Add citations

You must login to add citations.
  1. 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 and REGc. 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. The modal logic CPDLreg can serve as a technical foundation for reasoning about agency. Even very rich multi-agent logics can be embedded into CPDLreg via (...)
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  • Deciding Regular Grammar Logics with Converse Through First-Order Logic.Stéphane Demri & Hans De Nivelle - 2005 - Journal of Logic, Language and Information 14 (3):289-329.
    We provide a simple translation of the satisfiability problem for regular grammar logics with converse into GF2, which is the intersection of the guarded fragment and the 2-variable fragment of first-order logic. The translation is theoretically interesting because it translates modal logics with certain frame conditions into first-order logic, without explicitly expressing the frame conditions. It is practically relevant because it makes it possible to use a decision procedure for the guarded fragment in order to decide regular grammar logics with (...)
    Download  
     
    Export citation  
     
    Bookmark   3 citations  
  • 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