COOL – The Coalgebraic Ontology Logic Reasoner

(See also the COOL project page)

COOL is a generic reasoner for modal, hybrid and fixpoint logics, developed jointly at FAU Erlangen-Nürnberg and the Australian National University (Dirk Pattinson); it can be instantiated to any modal, hybrid or alternation-free fixpoint 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), serial monotone neighborhood logic (the next-step logic of game logic GL), and coalition logic (the next-step logic of alternating temporal logic ATL). COOL currently supports global assumptions, i.e. general TBoxes, nominals, satisfaction operators; the latter features are similar in expressivity to Boolean ABoxes. COOL implements two global caching algorithms as separate reasoner cores: the global caching algorithm described in this paper (also available here) and the global caching algorithm for alternation-free fixpoint logics described in this paper; the latter reasoner core decides the alternation-free mu-calculi over all supported logics (including in particular CTL, ATL and the star-nesting free fragment of GL). Recently, the fixpoint core has been extended with support for aconjunctive mu-calculi via permutation games, as described here; an archive containing according binaries, a formula generator and benchmarking scripts is available here.


The COOL source code and further documentation can be found on the COOL project page; Alternatively, here is a tarball of a snapshot. The sources of the global caching solver for alternation-free and aconjunctive mu-calculi can currently be found in separate branches of the repository. There also are

Experimental Results

Recent benchmarking results that compare MLSolver with the permutation game solving core of COOL for aconjunctive formulas can be found in this file:

We also compare the runtimes of three variants of the CTL-instantiation of the alternation-free fixpoint-reasoning core of COOL (with different frequencies of intermediate propagation – always, never and adaptive) with TreeTab and GMUL on various series of CTL formulas; for descriptions of the benchmark formulas and the provers TreeTab and GMUL, see An Experimental Comparison of Theorem Provers for CTL, R. Goré, J. Thomson and F. Widmann, TIME 2011. More benchmarking results can be found in this file: