zenon

Zenon is an extensible authomated theorem prover whose main claim to fame is that it produces actual proofs of theorems. Correctness is an explicit non-goal in the design of Zenon: the proof output needs to be checked by another program before the theorem is considered proved. As a consequence, Zenon is not designed for direct use by humans, but rather for interfacing into formal proof systems, such as interactive proof assistants and non-interactive proof checkers.