Track:
Papers Submitted to the Workshop
Downloads:
Abstract:
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.