Algebraic Reasoning with Prover9

Proof Database
We have built a basic proof database, 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.
We thank B. Möller, G. Schmidt and G. Struth for their contribution and their support.
Generated Models
Furthermore, we have generated a library of small models with Mace4 for Mace4 searches for finite structures satisfying first-order and equational statements, the same kind of statement that Prover9 accepts. it is also developed by William McCune.
Data for Selected Papers
For some paper we provide special data. Click at the title to access the data.
©2007—2013. Peter Höfner
last update: April, 8