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://cal8.cs.fau.de/cool