Questions and Answers for the MPTP Challenge
Questions about the selected problems
What is the difference betwen the first distribution and the current one?
Fixing several bugs in the problems, and making the distribution more usable.
Duplicate axioms in several problems were corrected, and some chainy problems where the conjecture
appeared also as a lemma were fixed. The one line versions of problems (suitable for simple utilities
like grep, etc.) were complemented with indented and better readable versions.
Why are some axioms just $true?
Such formulas exist to keep the bookkeeping when translating from Mizar to ATP simple.
It would be easy to delete them, but we do not do it for two reasons. First, $true (or $false)
have equivalent syntax in Mizar, so it can really happen that a Mizar user intended to write just $false
(e.g. while proving by contradiction). Second, $true and $false are now TPTP standard, and
systems should implement that standard.
Why are there fictitious variables?
Like the "B" in "fof(reflexivity_r1_tarski,axiom,( ! [A,B] : subset(A,A) ))."? Usually
these are formulas encoding Mizar 'properties" like "reflexivity". The Mizar data structure for them
allows for two variables (for properties like "symmetry"), and the translator did not care (yet) to remove
the fictitious one where allowed, because logically it does not matter. Generally, fictitious variables
are allowed both in TPTP and in Mizar, and good clausifiers should be able to deal with them.
Can I have a look at the original Mizar form of the problems?
Yes,
http://lipa.ms.mff.cuni.cz/~urban/xmlmml/html_abstr.930/00mptp_chall_topdown.html displays all the 252
conjectures from the root down to the leaves of the challenge tree. Mizar names like
FUNCT_1:34, XBOOLE_1:lemma 32, and XBOOLE_0:def 4 translate to TPTP as t34_funct_1, l32_xboole_1, and
d4_xboole_0. Clicking on the
proof keyword will display the whole Mizar proof.
Is there a system in naming the formulas?
Yes, see the previous answer for the main Mizar to TPTP name translation rules. The naming of
the formulas coming from various parts of the Mizar type system is also quite simple, but you probably
don't want to be bothered with the gory details of the Mizar's type system, and its translation to
TpTP.
Is there a system in naming the problems?
Yes, a problem named compts_1__t13_compts_1.p has as a conjecture a formula named t13_compts_1, you can rely on that.
The compts_1 part is the name of the original Mizar article, and t13 says that it is the thirteenth theorem
in that article.
How do I find a Mizar name and definition for a given symbol in the challenge files?
Search for it in the table of
NiceConstructorNames, and click on the link next to it.
Are symbol names and formula names used consistently across various problems?
Yes, every formula name denotes the same formula in all bushy and chainy problems, and every predicate and functor symbol has the same definition and properties there.
Allowed tuning
Is general pre-tuning on the TPTP Problem Library allowed?
Yes, any general system optimization done on TPTP which is allowed for CASC is allowed as pre-tuning.
Is general pre-tuning on the MPTP Problem Library allowed?
It has to be really general. Since the MPTP Challenge is a subset of MPTP, more detailed pre-tuning
will be considered as cheating, and should be left for the execution time. In other words, one substantial purpose of the
challenges is to support research in ATP tuning for various domains, and that's why such algorithms have to run
within the same execution limits, not in incomparable environments at each developer's labs.
Can systems do any retuning during execution?
Well, any retuning which only uses information computed from the problems during execution.
You cannot bring with your system a table of pre-computed results, and tune your system to it
during execution, but you can tune it by the table of results which you obtain during execution.
Can systems use information found in the bushy division to solve problems in the chainy division?
Absolutely not. The divisions are completely separate, ans serve different purposes.
Using information from one division to help the other would defeat this purpose.
System parts
I have a good CNF prover, is there a good clausifier I could plug in?
One very fast, good, and TPTP compliant is Stephan Schulz's, coming with eprover. Just run
eprover --cnf --tstp-format problem.fof > problem.cnf
One of the best, but not so fast on large problems is FLOTTER, coming with SPASS, which unfortunately
does not understand the
TpTP syntax. To make it work with the TPTP syntax, you can use Josef Urban's
hacked FLOTTER version
FlotterOnTPTP.
That distribution needs to be recompiled for non-linux systems (read the README, and run
"./FlotterOnTPTP.pl --man" for that).
I have a good machine learning or other metasystem, what ATP should I plug in?
Check the recent
CASC
results
(note that the MPTP problems are only FOF, so that division is the most relevant). Also the first
MPTP Challenge results
contain only ATP systems (no metasystems so far, but it can change).
Note that some systems can be hard to use for simple machine learning, as they do not easily
provide names of the axioms used in the proofs that they found (complain loudly to their authors).
Techniques
Is lemmatization allowed?
Yes, it is allowed to add lemmas proved from a problem's axioms as new axioms to the problem
(note that the TPTP formula role "lemma" is then more appropriate than just "axiom" - see the TPTP syntax at
http://www.cs.miami.edu/~tptp/TPTP/SyntaxBNF.html#formula_role for details).
It does not matter how the lemma was found (e.g. in the original problem, or in other problem, or it was just conjectured and proved),
but it should be clear (best by providing a proof), that the lemma really follows from the original problem's axioms.
Miscellaneous
Where does the money come from?
The money comes from Josef Urban's funding. If you are interested in offloading some of
your millions into a support of worthy AI research, please email the organizers.
--
JosefUrban - 10 Nov 2006
to top