An ExpTime Procedure for Description Logic $\mathcal{A}\mathcal{LC}\mathcal{Q}\mathcal{I}$ (Draft)

Yu Ding

A worst-case ExpTime tableau-based decision procedure is outlined for the satisfiability problem in $\mathcal{A}\mathcal{LC}\mathcal{Q}\mathcal{I}$ w.r.t. general axioms.