Re: proof objects for mizar: already available?

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 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/