An automatic theorem prover in OCaml for typed higher-order logic with equality and datatypes, based on superposition+rewriting; and Logtk, a supporting library for manipulating terms, formulas, clauses, etc.

[frozen] Scheduling and running jobs on a shared computer, then analyse their output

A kernel using inference rules in order to compute the three of proves.

An interpreter for an imperative language and a Hoare logic prover