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.
Notes
-
If you give a Prover9 output file, the server runs "prooftrans ivy" on it
to translate the proofs to Ivy proof objects.
Then, the Ivy checker is run on the proof objects.
-
Ivy accepts a different input language from Prover9, and the "prooftrans"
translation of the proof can change the meaning of the theorem in some cases.
The main points:
-
Prover9 is case-sensitive, and Ivy is not. This means, for
example, that if Prover9 were to (incorrectly) say
that "a != A" is a contradiction, Ivy would agree.
-
Some symbols accepted by Prover9 are not accepted by Ivy; we catch
and translate some of those. For example, "^" is mapped to "meet_for_ivy".
This kind of 2-to-1 mapping can cause the same kind of problem as
in the preceding point.
-
To be sure about cases like these, you can look at the proof
objects and check that the steps marked "(input)" really represent the
problem.
-
Ivy [1] was constructed in the
ACL2 proof development environment.
It is written in the ACL2 (Lisp-like) programming language,
and several soundness properties have been proved about it.
-
Although we don't know of any unsound proofs produced by a released
version of Prover9, we recommend using Ivy to check important proofs.
References
-
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.