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).
In addition to that COOL also handles many kinds of combinations of these basic logics:
- Choice A + B: Any world in the model can either have successors according to logic A or to logic B.
- Fusion A * B: Any world in the model has both successors according to logic A and to B.
- Sequence A . B: Any wolrd in the model has successors reachable by doing an A-step and then an B-step. (e.g. simple Segala systems which perform an nondeterministic step followed by an probabilistic step).
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.
If you have any questions or patches, feel free to send them via E-Mail.
An abortive attempt by Ulrich R. to formalize de Groote's paper
Coq formalization of guarded iteration a la https://www8.cs.fau.de/_media/research:papers:elgot-retract.pdf.
- Public Git:
git clone git://git8.cs.fau.de/enguard
- Member Git:
git clone email@example.com:enguard
- Public Git:
Utabcert is a Coq formalization of equivalence and containment results obtained by Sagiv and Yannakakis (Equivalence Among Relational Expressions with the Union and Difference Operators).
Under the assumption of the results of a recent ESOP paper (A Coq Formalization of the Relational Data Model. V Benzaken, É Contejean, S Dumbrava.) it provides:...
Also available in: Atom