Project

General

Profile

Wiki » History » Version 10

« Previous - Version 10/17 (diff) - Next » - Current version
Thorsten Wißmann, 04/29/2014 11:41 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.

Download

To get COOL, clone the git repository via:

git clone git://cal8.cs.fau.de/cool

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

Compiling