
mSAT
mSAT is a modular SAT Solver written in OCaml. It is based on altergozero, a standalone version of the SAT solver used at one point in the automated theorem prover altergo. mSAT provides an ocaml functor to create an SMT Solver with userdefined types for terms and formulas, and solving functions. Instantiating the functor with an empty solving function results in a pure SAT solver. mSAT also implements the McSat calculus.

Dolmen
Dolmen is an OCaml library that provides parsers for some languages used in automated deduction, such as TPTP and SMTLib. Besides providing already written uptodate parsers, another benefit of Dolmen is to document the various term structure needed for each language, and to provide an adequate implementation that meets these requirements.

Zenon Arith
Zenon Arith is an extension of the tableauxbased automated theorem prover Zenon. This extension uses the simplex algorithm as a decision procedure to solve problems over rationals, and a branchandbound approach to solve problems over integers. This extension is also able to handle real linear arithmetic, which actually coincides with the rational fragment of linear arithmetic due to the syntactical restrictions of the TPTP input format for reals. This extension is able to output proof scripts for the Coq proof assistant for automated verification.

Ocamlsimplex
Ocamlsimplex is an ocaml implementation of the simplex algorithm. It currently only check for satisfiability of linear systems, but can outptu proof certificates for unsatisfiable results. It is the decision procedure used in the ZenonArith theorem prover.

Frogutils
Frogutils provides tools and libraries (in OCaml) for scheduling and running jobs on a shared computer, and then analyse their output. It also includes a tool that aims to ease the process of benchmarking automated theorem provers and storing their result in an easy to read and use json file.