Exptime Tableaux for ALC

Giuseppe De Giacomo, Francesco M. Donini, and Fabio Massacci

We devise a refined tableaux calculus that integrates the techniques used in PDL with tableaux, thus achieving a tableaux-based procedure working in simple exponential time. In a nutshell, traditional tableaux methods close a branch only by "first principles" (atomic clashes), whereas our enhanced tableau exploits previously proved inconsistencies as additional lemmata to decide that a branch can be closed without having to find the same atomic clashes again.

This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.