Optimizing Conditional Logic Reasoning within CoLoSS

Daniel Hausmann, Lutz Schröder

In: Thomas Bolander, Torben Braüner (Hrsg.). Methods for Modalities (M4M-6, 2009). Methods for Modalities (M4M-6) 6th Workshop on Methods for Modalities November 12-14 Kopenhagen Denmark Seiten 157-171 Electronic Notes in Theoretical Computer Science (ENTCS) 262 Elsevier Amsterdam 5/2010.


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.


Weitere Links

cond-coloss.pdf (pdf, 231 KB)

Deutsches Forschungszentrum für Künstliche Intelligenz
German Research Center for Artificial Intelligence