Tableau algorithm for ALC
= Tableau algorithm for ALC
A <concept satisfiability> procedure that expands concept labels into a graph, branches on disjunctions, creates witnesses for existential restrictions, propagates universal restrictions along existing edges, and tests for a <tableau clash>. General <TBoxes> require global constraints and a termination device such as <direct blocking in description logic>.