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.
If you have any questions or patches, feel free to send them via E-Mail.