Re: proof objects for mizar: already available?

On 2011-10-09 11:56:29 +0000, Josef Urban said:

> On 10/9/11, Jesse Alama <[email protected]> wrote:
>> On 2011-10-01 09:26:45 +0000, Josef Urban said:
>> 
>>> On 10/1/11, Jesse Alama <[email protected]> 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 whole (completed) proofs are in one formalism: TPTP format with
> assumptions (see the paper).

The TPTP notation for derivations is a strong start, certainly.  
Looking at the paper, I see that they have a richer structure than I 
thought they had.

> 
>>> 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
> 
> There are indeed various choice points when translating from Mizar to
> pure first-order logic, but their default solutions have been provided
> in MPTP since 2005. See
> http://www.springerlink.com/content/kw9075426q26pu32/ . "set foo =
> bar" is just a syntactic macro in Mizar, so already Mizar semantic
> layer is "the set = the set", there is not really much of a choice
> here. The choice comes when translating "the" (Hilbert's epsilon) to
> first-order logic. This is not described in the paper above, because
> "the" came later in Mizar (2009?). But its default translation is very
> similar to translation of Faenkel terms (de-anonymization).

Well, semantically the fragment

set X = the set;
X = X

may simply be the equation "the set = the set", but it isn't the case 
that one can simply eliminate all 'set' statements from the MML by 
substituting the right-hand sides for free occurrences of the left-hand 
side.  If we really were to have natural deductions for mizar proof 
objects, I'd prefer the approach of introducing a universal formula to 
deal with 'set' statements, because then one could have a label for the 
equation

  X = the set

and obtain find-grained information about where this equation is 
needed.  Simply uniformly plugging in the right-hand side for the 
left-hand side would, in general,  produce unreadable proofs.  I'd like 
ideal proof objects which don't yet exist to record this information.  
Working with "semantic mizar proofs" (for lack of a better term) -- 
ones where macro substitution is absent because it has already been 
carried out -- is (at least) one step too far, to my taste, since we've 
lost some information in the mizar text.

> 
> To sum up: there is a default TPTP translation both of the Mizar
> natural deduction proof format and of the Mizar extensions over
> first-order logic, and both have been around and productively used for
> a couple of years now.

From my point of view, this is just the first step.  To my knowledge, 
we still lack even one bona fide natural deduction proof -- consisting 
exclusively of axioms of set theory, equality, and introduction and 
elimination of connectives -- of any (non-trivial) mizar theorem.  
Would you agree, or am I missing something?

> 
> But I'd be happy to see a continuation of the 2008 cross-verification
> paper that would attempt ATP-based cross-verification of the full MML
> (not just large random parts of it). Based on that (on the full proof
> objects), it would be probably fairly easy to import MML into HOL
> Light, Isabelle, Coq, ..., and that could in turn trigger further work
> on communication between the libraries of these systems.

Portability of the library is certainly one ripe fruit of such an 
export.  My own interest is in foundations.  There are all sorts of 
experiments that I'd like to carry out on a library of natural 
deduction proofs of genuine mathematical results, which, as far as I 
can see, I can't carry out with the TPTP derivation notation.  (I'm 
happy to concede that some of this is simply due to my ignorance of the 
details of TPTP derivations.)

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