COOL -- A Generic Satisfiability Checker For Coalgebraic Logics with Global Assumptions (System Description)

ABSTRACT. We describe the Coalgebraic Ontology Logic solver COOL, a generic reasoner that decides the satisfiability of modal formulas (with nominals) with respect to a set of global assumptions --a TBox in Description Logics parlance. The level of generality is that of coalgebraic logic, a logical framework covering a wide range of modal logics, beyond relational semantics. The core of COOL is an efficient unlabelled tableaux search procedure using global caching. Concrete logics are added by implemening the corresponding (one-step) tableaux rules. The logics covered at the moment are (multi-modal) K and KD (i.e., serial relations), graded modal logic and Pauly's Coalition Logic (the next-step fragment of Alternating-time Temporal Logic), plus every logic that arises from the above as a product (modal fusion) or coproduct of the underlying functors, which are handled automatically in a generic way. We compare the performance of COOL with state-of-the-art reasoners.