The checker is currently broken due to a Web server upgrade. Please check back later.

Checking Prover9 Proofs with Ivy

This page uses the Ivy proof checker to check Prover9 proofs. (This runs Ivy on our server, so you don't have to install it.)

Say you have a Prover9 output file (version at least September-2006) containing one or more proofs.

Use the "Browse" button below to locate the file on your computer, then click the "Upload File and Check Proofs" button.

Type of File:
Prover9 Output (example)
Old Prover9 Output (before version May-2007)
Ivy Proof Objects (example)
Show Proof Objects



  1. W. McCune and O. Shumsky, "Ivy: A Preprocessor and Proof Checker for First-order Logic". Chapter 16 in Computer-Aided Reasoning: ACL2 Case Studies (ed. M. Kaufmann, P. Manolios, and J Moore), Kluwer Academic Publishers, 2000.