Initial Readme from chair page on COOL

Many links are currently broken or not very useful but they are left
as is from the page

README.md

+# COOL -- The Coalgebraic Ontology Logic Reasoner
+
+[[_TOC_]]
+
+COOL is a generic reasoner for modal, hybrid and fixpoint logics, developed jointly at FAU Erlangen-Nürnberg and the Australian National University ([Dirk Pattinson](http://users.cecs.anu.edu.au/~dpattinson/)); it can be instantiated to any modal, hybrid or alternation-free fixpoint 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), serial monotone neighborhood logic (the next-step logic of game logic GL), and coalition logic (the next-step logic of alternating temporal logic ATL). COOL currently supports global assumptions, i.e. general TBoxes, nominals, satisfaction operators; the latter features are similar in expressivity to Boolean ABoxes. COOL implements two global caching algorithms as separate reasoner cores: the global caching algorithm described in [this paper](http://link.springer.com/chapter/10.1007/978-3-642-14203-1_5) (also available [here](/wp-content/uploads/staff/schroeder/papers/hyGlobalCaching.pdf)) and the global caching algorithm for alternation-free fixpoint logics described in [this paper](http://drops.dagstuhl.de/opus/volltexte/2016/6172/pdf/LIPIcs-CONCUR-2016-34.pdf); the latter reasoner core decides the alternation-free mu-calculi over all supported logics (including in particular CTL, ATL and the star-nesting free fragment of GL). **Recently, the fixpoint core has been extended with support for aconjunctive mu-calculi via permutation games, as described [here](https://arxiv.org/pdf/1710.08996.pdf); an archive containing according binaries, a formula generator and benchmarking scripts is available [here](/wp-content/uploads/media/research/cool/artifact.zip).**
+
+
+## Downloads 
+
+Alternatively, here is a [tarball](/wp-content/uploads/media/research/cool/cool-src-2014-02-01.tar.gz) of a snapshot. The sources of the global caching solver for [alternation-free](https://git8.cs.fau.de/software/cool) and **aconjunctive** mu-calculi can currently be found in separate branches of the repository. There also are
+
+- a 64 bit linux build of COOL [cool-bin-x86_64.tar.gz](/wp-content/uploads/media/research/cool/cool-bin-x86_64.tar.gz) (2014-02-01);
+- a 64 bit linux build of COOL including the alternation-free fixpoint solving core [cool-afmu-2016-05-24.tgz](/wp-content/uploads/media/research/cool/cool-afmu-2016-05-24.tgz) (2016-05-24).
+- a 64 bit linux build of COOL **including the aconjunctive fixpoint solving core** [cool-x86-64-2017-11-07.zip](/wp-content/uploads/media/research/cool/cool-bin-x86_64.tar.gz/cool-x86-64-2017-11-07.zip) (2017-11-07).
+
+## Experimental Results 
+
+**Recent benchmarking results that compare [MLSolver](https://github.com/tcsprojects/mlsolver) with the permutation game solving core of COOL for aconjunctive formulas can be found in this file: [benchmarks.zip](https://www8.cs.fau.de/_media/research:cool:benchmarks.zip)**
+
+We also compare the runtimes of three variants of the CTL-instantiation of the alternation-free fixpoint-reasoning core of COOL (with different frequencies of intermediate propagation -- *always*, *never* and *adaptive*) with TreeTab and GMUL on various series of CTL formulas; for descriptions of the benchmark formulas and the provers TreeTab and GMUL, see *An Experimental Comparison of Theorem Provers for CTL*, R. Goré, J. Thomson and F. Widmann, TIME 2011. More benchmarking results can be found in this file: [comparison_CTL.zip](https://www8.cs.fau.de/_media/research:cool:comparison_CTL.zip)
+
+## Literature 
+
+- A system description of COOL ([COOL --- A Generic Satisfiability Checker For Coalgebraic Logics with Global Assumptions](https://www8.cs.fau.de/_media/research:papers:cool.pdf), D. Gorin, D. Pattinson, L. Schröder, F. Widmann and T. Wißmann) has been published at [IJCAR 2014](http://cs.nyu.edu/ijcar2014/).
+- A paper on global caching for alternation-free fixpoint logics ([Global Caching for the Alternation-free µ-Calculus](http://drops.dagstuhl.de/opus/volltexte/2016/6172/pdf/LIPIcs-CONCUR-2016-34.pdf), D. Hausmann, L. Schröder and C. Egger) has been published at [CONCUR 2016](https://www.concur2016.ulaval.ca/no_cache/home/).