## Projects

- COOL
# 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.## Feedback¶

If you have any questions or patches, feel free to send them via E-Mail.

## Quick links¶

- Choice
- CORQUE
CORQUE stands for

*CORecursive eQUations over Effects*. This project contains a Coq formalization of complete Elgot monads, their corecursive extensions and background proofs for the paper Unguarded Recursion on Coinductive Resumptions... - countermachine
BSc project of Michael Banken on simulating counter machines

- cpscoq
An abortive attempt by Ulrich R. to formalize de Groote's paper

- dnegmod
A Coq formalization of "Negative Translations and Normal Modality".

To clone, use

git clone git://git8.cs.fau.de/dnegmod

- EnGuard
Coq formalization of guarded iteration a la https://www8.cs.fau.de/_media/research:papers:elgot-retract.pdf.

## Quicklinks:¶

- Public Git:
`git clone git://git8.cs.fau.de/enguard`

- Member Git:
`git clone gitolite@git8.cs.fau.de:enguard`

- Public Git:
- lw-simulator
BSc project of Alexander Dietsch for simulating LOOP and WHILE programs

- MBProg
Lecture notes on Monad-Based Programming

held by Dr. Sergey Goncharov in spring semester 2015.

### LaTeX source code¶

Obtaining the sources:

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

Preparing and sending patches:...

- ModuresErl
Paul Wild's development of Aarhus ModuRes library

To clone, use

git clone git://git8.cs.fau.de/ModuresErl

- puzzles
Material for the Chair presentation at

*50 Jahre TechFak*The assembled material (posters, simulations,...) can be found on https://www8.cs.fau.de/tf50:main

The train shunting simulation has its own project... - Ruitenburg 1984: cycles in IPC
This is a formalisation of Wim Ruitenburg's paper "On the Period of Sequences (An(p)) in Intuitionistic Propositional Calculus" (JSL 1984)

To clone, use

git clone git://git8.cs.fau.de/ruitenburg1984

- Shunting

A train shunting simulation for the browser: Try it online

For more material, see the Chair Homepage... - Utabcert
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