Optimal tableau algorithms for coalgebraic logics
Clemens Kupke
Info
|
Date |
31st May 2011 (week 5, Trinity Term 2011) |
|
Time |
11:30 |
|
Place |
147 |
Abstract
Tableau methods provide a versatile tool for automated reasoning in
modal and description logics. One drawback of
tableau-based decision
procedures is, however, that they often fail to meet the known
complexity bounds for the
logics in question. It has been shown that
optimality can be obtained for some logics by using a technique called
global caching.
In my talk I am going to demonstrate that global caching is applicable
to so-called coalgebraic
description logics that allow for reasoning
about number restrictions, probabilities and other variations to the
usual relational semantics. Furthermore I will discuss the close
connection between tableaux and automata for (coalgebraic)
modal logics.
This is joint work with R. Gore, D. Pattinson and L.Schroeder.
Further info
|
Related series |
|
