Cut-Free ExpTime Tableaux for Checking Satisfiability of a Knowledge\n Base in the Description Logic SHI

2011/06/12 by Linh Anh Nguyen, Nguyen, Linh Anh
Computer Science · #Advanced Database Systems and Queries #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Natural Language Processing Techniques #Semantic Web and Ontologies

paper · pdf · doi:10.48550/arxiv.1106.2305

openalex publication_date 2011/06/12 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

Abstract

We give the first cut-free ExpTime (optimal) tableau decision procedure for\nchecking satisfiability of a knowledge base in the description logic SHI, which\nextends the description logic ALC with transitive roles, inverse roles and role\nhierarchies.\n

Related

• ExpTime Tableaux with Global Caching for the Description Logic SHOQ
• ExpTime Tableaux for the Description Logic SHIQ Based on Global State Caching and Integer Linear Feasibility Checking
• An ExpTime Procedure for Description Logic ALCQI (Draft)
• A Cut-Free ExpTime Tableau Decision Procedure for the Logic Extending\n Converse-PDL with Regular Inclusion Axioms
• Optimal and Cut-free Tableaux for Propositional Dynamic Logic with\n Converse