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 largerscale 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:

D. Pattinson and M. Tiwari, Schulze Voting as Evidence Carrying
Computation.
[.pdf ]
Developers
 M. Tiwari, The Australian National University
 D. Pattinson, The Australian National University
Formally Verified Invariants of Vote Counting Schemesf
We use the approach of vote counting as mathematical proof (see
below) to show that a rulebased 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:

F. Verity and D. Pattinson, Formally Verified Invariants of Vote
Counting Schemes.
[.pdf ]
Developers
 F. Verity, Australian National University
 D. Pattinson, Australian National University
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:

D. Pattinson, Vote Counting as Mathematical Proof.
[.pdf ]
Developers
 D. Pattinson, Australian National University
COOL  The Coalgebraic Ontology Logic Reasoner
COOL is a generic reasoner for modal and hybrid logics, developed
jointly at FAU ErlangenNürnberg and the Australian National
University (Dirk Pattinson); it can be instantiated to any modal or
hybrid logic admitting an axiomatization in terms of socalled
rank1 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 nextstep 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
 Daniel Gorin, FAU ErlangenNuernberg
 Dirk Pattinson, The Australian National University
 Lutz Schroeder, FAU ErlangenNuernberg
 Florian Widmann
 Thorsten Wissmann, FAU Erlangen Nuernberg
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:

L. Schröder and D. Pattinson.
PSPACE bounds for rank1 modal logics.
ACM Transactions on Computational Logics, 10(2), 2009.
[ bib 
.pdf ]

W. Snell, D. Pattinson, and F. Widmann.
Solving graded/probabilistic modal logic via linear inequalities,
2011.
[ bib 
.pdf ]
Developers
 William Snell, Imperial College London
 Dirk Pattinson, Imperial College London
 Florian Widmann, Imperial College London
ICODESolvers
ICODEsolvers is a C package, which solves initial value problems,
using interval arithmetic and rational arithmetic packages. The
package contains programs based on domiantheoretic 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
 A. Edalat and D. Pattinson.
A domaintheoretic account of Picard's theorem.
LMS Journal of Computation and Mathematics, 10:83118,
2007.
[ bib 
.pdf ]
 A. Edalat and D. Pattinson.
A domain theoretic account of Euler's method for solving initial
value problems.
In J. Dongarra, K. Madsen, and J. Wasniewski,
editors, Proc.
PARA 2004, volume 3732 of Lecture Notes in Comp.
Sci., pages 112121,
2006.
[ bib 
.pdf ]
Developers
 Abbas Edalat, Imperial College London
 Ali Khanban, Imperial College London
 Dirk Pattinson, Imperial College London
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
nondeterminism and probabilities in different ways.
Download
Please note the
DISCLAIMER.
Documentation
The following system description gives an overview of the CoLoSS
system.
 G. Calin, R. Myers, D. Pattinson, and
L. Schröder.
ColoSS: The coalgebraic logic satisfiability solver.
Electr. Notes Theor. Comput. Sci., 231:4154, 2009.
Proc. Methods for Modalities 5 (2007).
[ bib 
.pdf ]
Developers
 Georgel Calin, Jacobs University Bremen, Germany
 Rob Myers, Imperial College London
 Dirk Pattinson, Imperial College London
 Lutz Schröder, DFKI Lab Bremen and Universität Bremen, Germany