Optimizing Conditional Logic Reasoning within CoLoSS (bibtex)

by Daniel Hausmann and Lutz Schröder

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.

Reference:

Daniel Hausmann and Lutz Schröder: Optimizing Conditional Logic Reasoning within CoLoSS, In Thomas Bolander, Torben Braüner, eds.: Methods for Modalities (M4M-6, 2009), Electronic Notes in Theoretical Computer Science, vol. 262, pp. 157–171, Elsevier; Amsterdam, 2010. [preprint]

Bibtex Entry:

@InProceedings{HausmannSchroder09,
  author = {Daniel Hausmann and Lutz Schr{\"o}der},
  title = {Optimizing Conditional Logic Reasoning within CoLoSS},
  year = {2010},
  editor = {Thomas Bolander and Torben Bra{\"u}ner},
  booktitle = {Methods for Modalities (M4M-6, 2009)},
  publisher = {Elsevier; Amsterdam},
  series = {Electronic Notes in Theoretical Computer Science},
  volume = {262},
  pages = {157-171 },
  keywords = {Coalgebraic modal logic conditional logic automated reasoning optimisation heuristics memoizing dynamic programming},
  comment = { <a href = "http://www8.informatik.uni-erlangen.de/~schroeder/papers/cond-coloss.pdf"> [preprint] </a>},
  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.
},
}