Re: [mizar] Re: calculating the transitive closure of required mizar items for a theorem

[Jesse Alama <alama@stanford.edu>]

Hi Josef,

Thanks for helping out with this.  It looks like the task of computing a
"custom MML" is going to require about as much effort as writing an
article. :->

Can you say more about how to use the MPTP system for doing one of the
recursive steps?  I'm interested in how (2) and (3) would work.

Option (1) may also work.  I would create one enormous MIZAR file
containing everything from the union of the articles metioned in the
environment of the article in which I prove x, and then write some code
to whittle away at the huge file until the removal of anything causes an
error which implies that the proof x is incorrect.

Thanks,

Jesse

Josef Urban <urban@ktilinux.ms.mff.cuni.cz> writes:

> Hi Jesse,
>
> sorry, I focused my reply on getting all article's external
> references, not on getting transitively all "things needed" for
> proving one theorem.
>
> Getting transitively all REFERENCES (theorems, schemes, definitions)
> used for a proof of one theorem is relatively easy, and you just apply
> one of the methods I described recursively (so I would definitely use
> the prolog (mptp) tools for this).
>
> Getting (transitively) ALL THINGS NEEDED (e.g. also registrations) for
> a proof of a theorem is quite difficult if you want to do it
> precisely. The options (speaking just about one step in the recursion)
> are:
>
> 1. Include all registrations mentioned in the theorem's article
> environment, plus all registrations preceding the theorem in its
> article. This is easy, but very imprecise.
>
> 2. Use MPTP's algorithm for creation of ATP reproving problems for the
> theorem (or for an older version of MML, just find the ATP problem at
> http://www.cs.miami.edu/~tptp/MizarTPTP/). It cuts down the redundant
> registrations using syntactic criteria, while still saying on the safe
> side.
>
> 3. Solve the ATP reproving problem using and ATP system, and look
> which registrations were actually used in the proof. This is much more
> precise, but sometimes hard to do, and also the set of "registrations
> necessary for an ATP proof" may slightly differ from those needed for
> the Mizar proof.
>
>
> There are other "things needed" which are analogous to the
> registrations (no easy documentation of their usage by the verifier),
> e.g. definitional expansions done in the Checker module. The possible
> solutions suggested above also apply to them.
>
> Josef
>
>
> On Tue, 6 Nov 2007, Jesse Alama wrote:
>
>> Hi Josef,
>>
>> This looks great -- thanks.  I'm a bit unclear on how to use the results
>> of these tools.  And in any case, if I understand correctly, this solves
>> only part of the problem I have in mind.
>>
>> I'd like to start with a theorem, say x, and prepare a customized MML
>> that consists of exactly those MIZAR items that are used to get x.  The
>> idea is to compute the smallest set S of MIZAR items such that if any
>> item were taken away from S, there would no longer be a MIZAR proof of x
>> or x would no longer be a well-formed formula.
>>
>> It seems to me that the tools you mention go some way toward achieving
>> this, but it seems that they go only one step of the way.  But perhaps
>> I'm misunderstanding something about the tools.  Can you clarify?
>>
>> Thanks much,
>>
>> Jesse
>>
>> Josef Urban <urban@ktilinux.ms.mff.cuni.cz> writes:
>>
>>> One option is just to grep article's XML form for "Ref" (postprocess
>>> the XML with addabsrefs.xsl first, to get absolute names of
>>> refrences). Throw away those which do not have the @articlenr
>>> attribute (these are local references). A formally more correct way
>>> would be to use an XPath expression (//Ref[@articlenr]) (see
>>> e.g. http://kti.ms.mff.cuni.cz/cgi-bin/viewcvs.cgi/mizarmode/Consider.pl?rev=1.2&view=auto)
>>> on the XML, but in this case grep is enough, because the Refs occupy
>>> always exactly one line in the XML. Of you also want schemes, grep
>>> also for "From".
>>>
>>> Another option is to additionally postprocess the XML with mizpl.xsl
>>> (all these stylesheets are at
>>> http://kti.ms.mff.cuni.cz/cgi-bin/viewcvs.cgi/xsl4mizar/), and use
>>> prolog on the resulting TPTP formulas. Again an easy way is just to
>>> find there all symbols of the form [tds][0-9]+_articlename . With some
>>> knowledge of the TPTP format, it should be easy to figure out where
>>> the references reside in the data, and thus which
>>> theorem/registration/definition uses them. (Again, this is also easy
>>> using and XPath expression directly on the XML).
>>>
>>> Josef
>>>
>>> On Mon, 5 Nov 2007, Jesse Alama wrote:
>>>
>>>> I'd like to start with a proof of a theorem in MIZAR and calculate the
>>>> transitive closure of the "x uses y" relation for both local articles
>>>> and articles in the MML.  What I have in mind is not only the transitive
>>>> closure of the "refers to" relation (the proof of x uses y), but also
>>>> things like registrations and proofs of existence and uniqueness for
>>>> functors, etc.  What tools can I use for this purpose?  I'm prepared to
>>>> write some code to help me with this, but I thought I'd ask the list to
>>>> see whether anyone knows how this might be accomplished with existing
>>>> tools (e.g., mmlquery).  Any ideas?
>>>>
>>>> Thanks,
>>>>
>>>> Jesse
>>>>
>>>> --
>>>> Jesse Alama (alama@stanford.edu)
>>>>
>>>
>>
>> -- 
>> Jesse Alama (alama@stanford.edu)
>>
>>
>

-- 
Jesse Alama (alama@stanford.edu)