Using tableau to decide description logics with full role negation and identity

DOI10.1145/2559947zbMath1287.03031arXiv1208.1476OpenAlexW3122242939MaRDI 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

zbMATH Keywords

complexitycompletenessdecidabilityblockingdescription logicBoolean modal logicidentity rolerole negationtableau-based reasoning

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Logic in artificial intelligence (68T27) Mechanization of proofs and logical operations (03B35)

Related Items

A bi-intuitionistic modal logic: foundations and automation ⋮ Modal Tableau Systems with Blocking and Congruence Closure ⋮ Using tableau to decide description logics with full role negation and identity ⋮ Blocking and other enhancements for bottom-up model generation methods ⋮ Modal Satisfiability via SMT Solving

Uses Software

• SPASS
• E Theorem Prover
• MetTeL
• KL-ONE

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• 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