Algebraic Reasoning with Prover9

This page provides a link to a basic proof database, maintained by Peter Höfner, that contains the Prover9 input and output files of proof experiments with Prover9 is a resolution- and paramodulation-based automated theorem prover developed by William McCune.

If you want to contribute to the proof database, please send us your input files and any information that will help us to replay your proofs.

An Isabelle repository for relational and algebraic methods can be found via this link.