Wiki » History » Version 13

« Previous - Version 13/17 (diff) - Next » - Current version
Thorsten Wißmann, 04/29/2014 11:49 PM

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). 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.


To get COOL, clone the git repository via:

git clone git://
The compilation of COOL is described in the shipped INSTALL file. It also lists the build-time and run-time dependencies.

A January snapshot of COOL is also available as static 64-bit linux binaries and static 32-bit linux binaries.

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