Proof Problems from the Mizar Library
Downloadable Problem Sets
Proof problems extracted from the Mizar Library can be downloaded in TPTP first order
format.
The first problem set is from the Mizar article ``Boolean Properties
of Sets'' and involves only the most general Mizar type ``set'' which
therefore could be eliminated.
The second set is from the Mizar article ``Relations Defined on Sets''
and involves several different types, which are encoded as
relativizations for compliance with the current version of the TPTP
syntax.
ILF Proof Presentation Service
Proofs of the ``boole'' problem set from the systems KoMeT, Protein, Setheo and Otter are
translated into ordinary mathematical notation by the ILF Mail
Server, if the TEXOP section of the input mail contains the line
"TEXOP USE mizar!boole".
Problems and progress should be reported to the ILF group.