# COOL - The Coalgebraic Ontology Logic Reasoner¶

COOL is a generic reasoner for modal and hybrid logics; it can be instantiated to any modal or hybrid logic admitting an axiomatization in terms of so-called rank-1 rules or axioms. Current instantiations include multimodal K (i.e. the description logic ALC), graded modal logic (the Q in ALCQ), and coalition logic (the next-step logic of alternating temporal logic ATL).

In addition to that COOL also handles many kinds of combinations of these basic logics:

- Choice
*A + B*: Any world in the model can either have successors according to logic*A*or to logic*B*. - Fusion
*A * B*: Any world in the model has both successors according to logic*A*and to*B*. - Sequence
*A . B*: Any wolrd in the model has successors reachable by doing an*A*-step and then an*B*-step. (e.g. simple Segala systems which perform an nondeterministic step followed by an probabilistic step).

COOL currently supports global assumptions, i.e. general TBoxes, nominals, and satisfaction operators; the latter features are similar in expressivity to Boolean ABoxes. COOL implements a global caching algorithm described here (also available here).

A system description of COOL (*COOL -- A Generic Satisfiability Checker For Coalgebraic Logics with Global Assumptions*, D. Gorin, D. Pattinson, L. Schröder, F. Widmann and T. Wißmann) is forthcoming at IJCAR 2014.

## Feedback¶

If you have any questions or patches, feel free to send them via E-Mail.