[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
[mizar] Explaining Mizar atomic inferences
Hi,
On Thu, 10 Apr 2008, Josef Urban wrote:
This is quite subtle, I had to use an explanation provided by the E automated
theorem prover on your article to see it (hopefully I'll make this
functionality publicly available soon)
I have made the explanations of Mizar atomic inferences ("by") publicly
available at http://octopi.mizar.org/~mptp/MizAR.html . It works by
- submitting an article (it will run Mizar, produce HTML, and produce ATP
problems corresponding to the "by" steps)
- clicking on the "by" keywords (or just ";") that you want to explain
will then run an ATP system (currently E prover) on the problem with a
small time limit, and show the linked needed references if the proof was
found
- if the prover succeeded, clicking the IDV (palm tree) icon will launch
the IDV (http://web.cs.miami.edu/home/strac/projects/IDV/) java applet by
Steven Trac for browsing the ATP proof (java browser plugin is needed)
- the "Try more" link gives you a SystemOnTPTP
(http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTP) interface by Geoff
Sutcliffe, where different ATP systems, with different settings can be
tried on the translated problem
It is possible to use the interface also for finding proofs that are too
difficult for the Mizar checker, but the needed (additional) references
have to be provided in the Mizar article. Additional functionality for
suggesting suitable references (and running ATPs on them) will probably be
added later.
Please do not submit huge articles (or at least use @proof for the
irrelevant parts), and behave nicely, the functionality is very
experimental.
Comments, suggestions, and bug reports are appreciated,
Josef Urban