[Date Prev][Date Next] [Chronological] [Thread] [Top]

[mizar] Re: proof objects for mizar: already available?

On 2011-10-01 09:26:45 +0000, Josef Urban said:


On 10/1/11, Jesse Alama <jesse.alama@gmail.com> wrote:


(b) Proofs objects are already available, in some sense, for mizar
proofs.  They do not give precisely what is wanted from the
concept of proof object, though:

* They are not always available.  With the current transformation
into a vanilla first-order format, and with current ATPs, for
less than half of mizar theorems from the library do we have
deductions.  This is clearly an important result for the
community, but not having deductions is a serious shortcoming.
We want proof objects for all mizar proofs.


The "ATP proof object completion" used for ATP cross-verification of
Mizar in http://www.springerlink.com/content/b7383x43l55p1183/ does
not rely on re-proving whole Mizar theorems.

It is based on re-proving the Mizar "by" and "from" steps, where the
ATP success rate is (so far) over 99% , and on ATP verification of the
Mizar structural natural deduction steps, where the success rate is
(so far) 100%.
Nonetheless, the situation is not entirely satisfactory. What we have is a kind of hybrid proof: part is in the mizar proof formalism, and the other part is in the proof formalism of whatever ATP is used. From a proof-theoretic perspective from a mizar proof we find a natural deduction proof with lots of axioms (corresponding to its "by" steps). 





* The calculi of the proofs that are found this way depend on the
theorem prover employed.  One finds proofs in the superposition
calculi, resolution calculi... The plurality of proof calculi is
welcome -- we want to view mizar proof objects through various
formal lenses -- but none of these is satisfactory because none
is a natural deduction proof in the style of mizar.  (To some
extent this problem can be overcome: an ATP could either do
search in a natural deduction setting, or emit natural
deductions by translating whatever calculus it uses into natural
deduction.  But proof search in natural deduction is generally
not as efficient as search in other calculi.  And the
translation from other calculi to a natural deduction is not
always clear.)  What is wanted from proof objects for mizar is a
sort of natural deduction proof that adheres more or less to the
mizar format, but which brings out all logical details.  It is
unpleasant and awkward to switch from natural deduction-style
mizar proofs to unnatural resolution deductions.


It is trivial to translate Prover9 proof objects to Mizar proofs, It
was done in 2003: https://github.com/JUrban/ott2miz . The translated
detailed proofs can be further post-processed by running the Mizar
native proof-improving ("irrelevant") utilities in a fixpoint loop
(this was added to Emacs mode on Freek's request in 2005).


I wasn't aware of this, thanks.





* There is no assurance that the proofs discovered by an ATP
thanks to Josef's translations are the same as the mizar proofs
with which one started.  Genuinely new proofs can be (and are)
discovered.  An ATP might exploit a premise or combination of
premises in an unusual way that diverges from the input mizar
proof.  An even when the ATP-discovered proof is more or less
congruent to the mizar proof from which it came, because it is
expressed in a different formal calculus there might be some
uncertainty about whether we are looking at the same proof.


This again is more about using ATPs to find new big proofs than about
reproducing the (typically quite limited) "by" steps.
I agree. Reproving individual "by" and "from" steps significantly diminishes the possibility that the proof that the mizar checker finds differs from the one discovered (in > 99% of cases) by an ATP. 


I totally agree that having detailed proof objects for all of MML
would be a great resource for study and data-mining of mathematical
proofs. The ATP path to this turned out to be very cheap once I had
practically complete ATP export and strong ATP methods.

Doing it the hard way inside Mizar is certainly possible (I have
partially done it in 2000), but it will be a serious amount of work on
Mizar, and even if you do it, it will be in a constant danger of
becoming obsolete by later re-implementations of parts of Mizar. Bill
McCune told me in 2004 that the detailed Otter proof objects were so
much added code that it lead him to reimplement the whole thing as
Prover9. My experience from 2000 with the Mizar kernel was similar: it
was a large blow-up of the code, and a cleaner complete rewrite would
be needed.
I agree that it probably would be a rather complex project to have bona fide proof objects for mizar. In addition to the problem of exposing "by"/"from" steps, there remains the problem of exporting a mizar proof -- even taking for granted that its "by" and "from" steps can be filled in some acceptable way, treating them as black boxes (or as axioms, in a natural deduction/sequent calculus context) -- into a vanilla natural deduction format. I think there are lots of design problems here. For example, consider the text fragment: 

set X = the set;
theorem X = X;

Do we translate this as the universal formula:

for X : set (X = the set --> X = X)

Or as the equation:

the set = the set
(Put aside for the moment the problem of translating "the set".) It won't do to say that these are "the same thing". They're equivalent, but that requires proof. The latter is generally taken as an axiom when reasoning with equality in natural deduction or sequent calculus; the latter is not (though perhaps it could be -- we might need to explore extensions of various calculi when deciding how proof objects should be represented). The universal requires an application of universal introduction (if we are working in a natural deduction setting), implication introduction, and an axiom of equality. 

--
Jesse Alama
http://centria.di.fct.unl.pt/~alama/