Teaching Projects Research PhD Topics Talks Publications Software Haskell
Here are some software packages that have been developed that actually bring theoretical ideas onto the machine. Mainly, these are concerned with exact real arithmetic, (modal) theorem proving and electronic voting. Within the COOL project, we did succeed to gain EPSRC funding to implement a larger-scale automated reasoning platform based on the coalgebraic paradigm that will extend the prototype below.

Schulze Voting as Evidence Carrying Computation

We present a specification of the Schulze Method as a dependent inductive type, and extract a provably correct program that counts votes according to the Schulze Method. The key point of our implementation is that it produces evidence (a scrutiny sheet, or transcript of the count) that can be independently verified.

Download

Please note the DISCLAIMER.

Documentation

The download above are the Coq sources that accompany the as of yet unpublished paper:

Developers

Formally Verified Invariants of Vote Counting Schemesf

We use the approach of vote counting as mathematical proof (see below) to show that a rule-based specification of vote counting schemes allows us to verify properties with relative ease. Using rule based counting schemes, we set up suitable invariants that propagate over vote counting rules. In particular, the invariant holds at the last step of counting, and so yields a formal proof of the property under consideration. We give two examples of properties that we formally prove by means of invariants: the monotonicity criterion for plurality voting, and the majority criterion for single transferable vote.

Download

Please note the DISCLAIMER.

Documentation

The download above are the Coq sources that accompany the as of yet unpublished paper:

Developers

Vote Counting as Mathematical Proof

We advocate that electronic vote counting should not only deliver a result but also an independently verifiable certificate of the correctness of the count. We have developed proof rules for vote counting that are implemented in the Coq code below. The use of program extraction gives a provably correct vote counting function that also produces independently verifiable certificates.

Download

Please note the DISCLAIMER.

Documentation

The implementation is based described in the (as of yet unpublished) paper:

Developers

COOL -- The Coalgebraic Ontology Logic Reasoner

COOL is a generic reasoner for modal and hybrid logics, developed jointly at FAU Erlangen-Nürnberg and the Australian National University (Dirk Pattinson); 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.

Download and Documentation

Please note the DISCLAIMER.

Developers

Graded and Probabablistic Modal Logic Solver

The code below implements the tableau calculus for both graded and probabilistic modal logic based on mixed integer programming. We are implementing a standard (unlabelled) tableau calculus, the rules of which are implemented with the help of mixed integer programming. Propositional connectives are represented using binary decision diagrams. The main novelty lies in the rules that have a similar format for both graded and probabilistic modal logic.

download

Please note the DISCLAIMER.

Documentation

The implementation is based on and described in the following papers:

Developers

IC-ODE-Solvers

IC-ODE-solvers is a C package, which solves initial value problems, using interval arithmetic and rational arithmetic packages. The package contains programs based on domian-theoretic versions of Picard's and Euler's methods to solve initial value problems. The installation method and a few examples are provided in this package in order to help the user. All feedbacks and comments should be sent to the email provided in the package.

Download

Please note the DISCLAIMER.

Documentation

The implementation is based on the papers

Developers

COLOSS: The Coalgebraic Logic Satisfiability Solver

COLOSS, the Coalgebraic Logic Satisfiability Solver, decides satisfiability of modal formulas in a generic and compositional way. It implements a uniform polynomial space algorithm to decide satisfiability for modal logics that are amenable to coalgebraic semantics. This includes e.g. the logics K, KD, Pauly's coalition logic, graded modal logic, and probabilistic modal logic. Logics are easily integrated into COLOSS by providing a complete axiomatisation of their coalgebraic semantics in a specific format. Moreover, COLOSS is compositional: it synthesises decision procedures for modular combinations of logics that include the fusion of two modal logics as a special case. One thus automatically obtains reasoning support e.g. for logics interpreted over probabilistic automata that combine non-determinism and probabilities in different ways.

Download

Please note the DISCLAIMER.

Documentation

The following system description gives an overview of the CoLoSS system.

Developers

Dirk Pattinson [check HTML] [check CSS]