ExpTime Tableaux for the Description Logic SHIQ Based on Global State Caching and Integer Linear Feasibility Checking

2012/05/25 by Linh Anh Nguyen, Nguyen, Linh Anh · 1 citation
Computer Science · #Logic, Reasoning, and Knowledge #Semantic Web and Ontologies #Formal Methods in Verification

paper · pdf · doi:10.48550/arxiv.1205.5838

Abstract

We give the first ExpTime (complexity-optimal) tableau decision procedure for checking satisfiability of a knowledge base in the description logic SHIQ when numbers are coded in unary. Our procedure is based on global state caching and integer linear feasibility checking.

Citations

• A near-optimal method for reasoning about action

Cited by

• ExpTime Tableaux with Global Caching for the Description Logic SHOQ

Related

• ExpTime Tableaux with Global Caching for the Description Logic SHOQ
• Cut-Free ExpTime Tableaux for Checking Satisfiability of a Knowledge\n Base in the Description Logic SHI
• An ExpTime Procedure for Description Logic ALCQI (Draft)
• Data complexity of answering conjunctive queries over SHIQ knowledge bases
• ExpTime Tableaux with Global Caching for Hybrid PDL