Abstract. We give an optimal (exptime), sound and complete tableaubased algorithm for deciding satisfiability with respect to a TBox in the logic ALCI using global state caching. ...
Abstract. I will begin by explaining an optimal tableau-based algorithm for checking ALC-satisfiability which uses "global caching" and which appears to work well in prac...