Using tableau to decide description logics with full role negation and identity
From MaRDI portal
Publication:5410334
DOI10.1145/2559947zbMath1287.03031arXiv1208.1476MaRDI QIDQ5410334
Dmitry Tishkovsky, Renate A. Schmidt
Publication date: 16 April 2014
Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1208.1476
complexity; completeness; decidability; blocking; description logic; Boolean modal logic; identity role; role negation; tableau-based reasoning
03B45: Modal logic (including the logic of norms)
68T27: Logic in artificial intelligence
03B35: Mechanization of proofs and logical operations
Related Items
Modal Satisfiability via SMT Solving, Using tableau to decide description logics with full role negation and identity, A bi-intuitionistic modal logic: foundations and automation, Blocking and other enhancements for bottom-up model generation methods, Modal Tableau Systems with Blocking and Congruence Closure
Uses Software
Cites Work
- A new methodology for developing deduction methods
- Tableau methods of proof for modal logics
- PSPACE Reasoning for Graded Modal Logics
- $\textsc{Met\hspace{-.5pt}TeL}$ : A Tableau Prover with Logic-Independent Inference Engine
- Automated Reasoning About Metric and Topology
- A General Tableau Method for Deciding Description Logics, Modal Logics and Related First-Order Fragments
- System Description: Spass Version 3.0
- Blocking and Other Enhancements for Bottom-Up Model Generation Methods
- Hypertableau Reasoning for Description Logics
- On languages with two variables
- On the Decision Problem for Two-Variable First-Order Logic
- Resolution-based methods for modal logics
- A general framework for pattern-driven modal tableaux
- Internalizing labelled deduction
- Automated Reasoning
- Using tableau to decide description logics with full role negation and identity
- Automated Synthesis of Tableau Calculi
- An overview of tableau algorithms for description logics
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
