5 found
  1.  79
    Analytic Tableau Systems and Interpolation for the Modal Logics KB, KDB, K5, KD.Linh Anh Nguyen - 2001 - Studia Logica 69 (1):41-57.
    We give complete sequent-like tableau systems for the modal logics KB, KDB, K5, and KD5. Analytic cut rules are used to obtain the completeness. Our systems have the analytic superformula property and can thus give a decision procedure. Using the systems, we prove the Craig interpolation lemma for the mentioned logics.
    Direct download (6 more)  
    Export citation  
    Bookmark   4 citations  
  2.  32
    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 (...)
    Direct download (7 more)  
    Export citation  
    Bookmark   1 citation  
  3.  18
    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 (...)
    Direct download (4 more)  
    Export citation  
    Bookmark   1 citation  
  4.  41
    Modal Logic Programming Revisited.Linh Anh Nguyen - 2009 - Journal of Applied Non-Classical Logics 19 (2):167-181.
    We present optimizations for the modal logic programming system MProlog, including the standard form for resolution cycles, optimized sets of rules used as meta-clauses, optimizations for the version of MProlog without existential modal operators, as well as iterative deepening search and tabulation. Our SLD-resolution calculi for MProlog in a number of modal logics are still strongly complete when resolution cycles are in the standard form and optimized sets of rules are used. We also show that the labelling technique used in (...)
    Direct download (5 more)  
    Export citation  
  5.  3
    On the Deterministic Horn Fragment of Test-Free PDL.Linh Anh Nguyen - 2006 - In Guido Governatori, Ian Hodkinson & Yde Venema (eds.), Advances in Modal Logic, Volume 6. CSLI Publications. pp. 373-392.
    No categories
    Direct download  
    Export citation  
    Bookmark   1 citation