| Publication type: |
Article in Proceedings |
| Author: |
Daniel Hausmann, Lutz Schröder |
| Editor: |
Thomas Bolander, Torben Braüner |
| Title: |
Optimizing Conditional Logic Reasoning within CoLoSS |
| Book / Collection title: |
Methods for Modalities (M4M-6, 2009) |
| Volume: |
262 |
| Page(s): |
157-171 |
| Series: |
Electronic Notes in Theoretical Computer Science |
| Year published: |
2010 |
| Publisher: |
Elsevier, Amsterdam |
| Abstract: |
The generic modal reasoner CoLoSS covers a wide variety of logics
ranging from graded and probabilistic modal logic to coalition logic
and conditional logics, being based on a broadly applicable
coalgebraic semantics and an ensuing general treatment of modal
sequent and tableau calculi. Here, we present research into
optimisation of the reasoning strategies employed in
CoLoSS. Specifically, we discuss strategies of memoisation and
dynamic programming that are based on the observation that short
sequents play a central role in many of the logics under
study. These optimisations seem to be particularly useful for the
case of conditional logics, for some of which dynamic programming
even improves the theoretical complexity of the algorithm. These
strategies have been implemented in CoLoSS; we give a detailed
comparison of the different heuristics, observing that in the
targeted domain of conditional logics, a substantial speed-up can be
achieved.
|
| PDF Version: |
http://www.informatik.uni-bremen.de/~lschrode/papers/cond-coloss.pdf |
| Keywords: |
Coalgebraic modal logic conditional logic automated reasoning optimisation heuristics memoizing dynamic programming |
| Status: |
Reviewed |
| Last updated: |
10. 05. 2010 |
