For those interested in automated theorem-proving, I'm pleased to announce a major advance in tools has occurred...
The Mizar library of formalized math has finally been translated into a sensible format, usable for training automated theorem-proving systems ;-) Josef Urban informed me that ***** I am now writing an extended version of a paper describing export of Mizar proofs to TPTP (see http://www.springerlink.com/content/t88848500815t188/ for the conference version), and have just remembered your request for having Mizar proofs exported to KIF or TPTP. So yes, I have translated it all to TPTP derivations, which can be ATP-verified by tools like GDV (see the paper). The page which presents it all is http://www.cs.miami.edu/~tptp/MizarTPTP/ , the TSTP icons there give you the TPTP derivations corresponding to each Mizar proof (see http://www.activemath.org/workshops/MathUI/07/proceedings/Urban-etal-MizarIDV-MathUI07.pdf for explanation of the site). If you want tar.gz of all the proofs, some version is at http://lipa.ms.mff.cuni.cz/~urban/nd_problems1.tar.gz (watch out, it is huge). There are still some completness bugs, the biggest is lack of explicit arithmetic evaluations done by mizar (inferences like 4+5=9 that dumb FOL ATP system will not prove), but otherwise it mostly works (see the paper). ***** TPTP, unlike Mizar syntax, is a small and straightforward BNF grammar which should be translatable into the internal KR of any AI system with a formal-logic-based aspect, with only moderate effort. So we can now import all of undergrad math and some grad-level math into AI systems, which provides the possibility of doing inductive reasoning on a large corpus of proofs to teach AI systems how to prove theorems... -- Ben G On Mon, 19 Mar 2007, Josef Urban wrote: > > > Ben, > > the MPTP export keeps at this moment quite a lot of the original Mizar proof > structure in the TPTP 'useful info' slot, but not all of it. Depending on > what kind of learning you want to do, it might or might not suffice. The > biggest ommission is probably the lack of further description of unproved > propositions (precisely in TPTP syntax: fofs with role 'unknown' and > mptp_info(_,_,proposition,_,_)). Most of them are probably natural deduction > (ND) assumptions, but some are not (e.g. propositions about constants > introduced by the 'consider' keyword - they can be rather thought of as > definitions). > > It should not be difficult to add the missing info there - the TPTP format is > produced directly from the XML, which contains all the proof structure. There > have been several reasons for postponing this so far - my focus on getting > the reproving of the simple steps right (which is sort of a precondition for > ATP cross-verification of Mizar, which in turn is a precondition for > productive use of deductive tools like ATP as part of larger knowledge-based > systems tailored for Mizar), and also a focus on getting the reproving of > theorems from their external references right, which in a sense gives you a > large-scale proof structure (which is not only usable for learning, but also > - unlike the ND internal proofs - understandable to ATPs, and thus allowing > things like the MPTP challenge). Another reason was that I did not want to > decide about the details of MPTP ND annotations, until I decided about the > export of ND proof structure to TPTP. The latter accidentally happened last > week (not only as a next step for the cross-verification, but also as a > megalomanic plan to build the detailed MML DAG with milions of nodes :-). So > some missing annotations will appear in the next few weeks (maybe even days), > and more importantly, the Mizar ND proofs will become TPTP proofs (if needed > without any ND - though there is a good chance that assumptions will become > acknowledged and processed parts of TPTP proofs). > > To sum up: > - you can have 'raw Mizar' loaded by using the XML - that gives you access to > the formulas and Mizar proof structure; the disadvantage is that for any > deductive tool which you might want to use, you'll have to define the > translation to its logic > - there is the 'raw MPTP', with formulas in extended TPTP syntax containing > the mptp_info annotations; this is sort of a middle way between the XML and > standard TPTP; the annotations are likely to get a bit better in near future, > what they annotate is still the Mizar ND structure > - there are pre-generated 'standard TPTP' problem sets in the MPTP distro and > the MPTPChallenge distro; these you can feed to ATP systems, and also > learning systems (the symbols and proposition names are stable there - always > the same semantics); for quite a lot of them an ATP proof can be found (and > used for learning) > - there will (hopefully soon) be a full TPTP (i.e. mostly/completely non-ND) > proof structure export, compatible with the proofs produced by ATP systems > like EP. > > Josef > > On Sun, 18 Mar 2007, Ben Goertzel wrote: > >> >> Josef, >> >> Thanks for your reply! However, I'm not sure we are fully understanding >> each other. >> >> I agree that the TPTP language has a level of simplicity similar to that of >> KIF, so that converting TPTP into KIF wouldn't be a big deal. >> >> And, from the point of view of my own Novamente AI system, writing a >> specialized TPTP loader and bypassing KIF wouldn't be a big deal either. >> >> However, I am not sure from your email if the "MPTP export" of Mizar, at >> this point, actually exports the **proofs** in the existing Mizar corpus >> (Journal of Formalized Mathematics), or just the theorem statements. Can >> you clarify? For my purposes, I need the proofs not just the theorems, as >> my desire is to do inductive learning of proof-patterns based on automated >> analysis of the proof-corpus. >> >> Thanks >> Ben Goertzel >> Novamente LLC >> [EMAIL PROTECTED] >> >> >> >>> >>> Hi Ben, >>> >>> On Sat, 17 Mar 2007, Ben Goertzel wrote: >>> >>>> >>>> Hi all, >>>> >>>> I am the leader of an AI project (www.novamente.net) and am interested >>>> to apply my AI system to automated theorem-proving based on a method >>>> of having it ingest the existing corpus of Mizar proofs, inductively >>>> infer >>>> "patterns of proof" therefrom, and then use these patterns to guide its >>>> work in further proofs. >>> >>> Good, hope you'll submit your system to the MPTP Challenge >>> (http://www.cs.miami.edu/~tptp/MPTPChallenge/), and write a paper about it >>> to ESARLT (http://www.cs.miami.edu/~geoff/Conferences/ESARLT/). >>> >>>> However, the first issue confronted along this path is that my AI system >>>> does not possess a Mizar loader. This is because Mizar's syntax is >>>> bloody complicated! (Understandably so, because of its design goals.) >>>> >>>> Thus, it seems necessary to convert Mizar to some simpler and more >>>> standard >>>> format. A sensible choice would seem to be KIF >>>> >>>> http://www.ksl.stanford.edu/knowledge-sharing/kif/ >>>> >>>> but of course other similarly simple formats would do as well. >>> >>> Mizar is translated to TPTP by the MPTP export >>> (http://kti.ms.mff.cuni.cz/~urban/MPTP2/mptp0.2.tar.gz). TPTP2KIF can be >>> probably achieved through TPTP2X from the TPTP distro (not that there >>> would be many "really running systems" fully implementing KIF (AFAIK)). >>> Also, just for initial learning experiments, the MPTPChallenge problems >>> (http://www.cs.miami.edu/~tptp/MPTPChallenge/MPTPChallenge.tgz) might be >>> enough. >>> >>>> My question is whether anyone has created a converter of this sort, or >>>> has >>>> thought seriously about it. >>>> >>>> If no one has created one, does anyone have an educated estimate >>>> regarding >>>> how long this task would take for an individual with suitable background >>>> in mathematics and software engineering? >>> >>> I hope that MPTP is enough for you, you are welcome to play with it and >>> improve it - there are number of ways how one can "translate" Mizar and >>> its proofs, e.g. with respect to optimizations available in various >>> reasoning systems, and I hardly did the "basic" approach so far. Also >>> Mizar is available in XML-ized format >>> (http://mmlquery.mizar.org/mizardoc/xml/Mizar.html) which solves the >>> low-level technical "loading" issue, and may be also usable e.g. for >>> machine learning (fo some hints read e.g. section 3.5 of >>> http://ktiml.mff.cuni.cz/~urban/mizxml.ps). However it is certainly still >>> "Mizar world", not a standardized well-known format like TPTP. >>> >>> Best regards, >>> Josef Urban >>> >> >> > ----- This list is sponsored by AGIRI: http://www.agiri.org/email To unsubscribe or change your options, please go to: http://v2.listbox.com/member/?member_id=8660244&id_secret=78811361-ac51a1
