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¶
- 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.
The main link is now https://git8.cs.fau.de/software/countermachine.
- cpscoq
An abortive attempt by Ulrich R. to formalize de Groote's paper
- dnegmod
A Coq formalization of "Negative Translations and Normal Modality".
This is not an updated link anymore. The repository has been moved to
https://git8.cs.fau.de/software/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. The repository has been moved to https://git8.cs.fau.de/software/lw-simulator and a successor tool is available as well: https://www8.cs.fau.de/tools:loopwhile.
- 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. The main link now is https://git8.cs.fau.de/software/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)
This is not an updated link anymore. The repository has been moved to https://git8.cs.fau.de/software/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