Note for Mizar Mailing List (fwd)

[Andrzej Trybulec <trybulec@math.uwb.edu.pl>]

---------- Forwarded message ----------
Date: Tue, 08 Dec 1998 14:01:38 +0100
From: dahn <dahn@uni-koblenz.de>
To: Andrzej Trybulec <trybulec@math.uwb.edu.pl>
Subject: Note for Mizar Mailing List

Hallo,

I distributed the following mail on several mailing lists.
Unfortunately, I forgot how to put it on the Mizar list. Please, forward
it for me.

Thank you

Ingo

-----------------------------

(With apologies for multiple copies.)

Christoph Wernhard has extracted all theorems from the Mizar article
"Relations Defined on Sets" by E. Woronowicz. (relset_1).  They have
been augmented by formulas that may have been used explicitely or
implicitely by the Mizar system for the verification of their proofs.
The resulting proof problems are available for download as first order
problems in TPTP format from

http://www-irm.mathematik.hu-berlin.de/~ilf/miz2atp/download.html

There are also more explanations on these problems and a presentation in

ordinary mathematical notation.

The Mizar article uses polymorphic types. They are easily recognised in
the chosen translation into first order logic. It is NOT the goal, to
solve the problems in the form in which they are submitted. Rather,
automated provers should be enabled to make efficient use of the
available type information.

Difficulty:
Otter solved 25 out of the 47 problems in automode. For the remaining
problems I needed in most cases 3-4 interactions with the interactive
theorem prover ProofPad which was powered by the automated provers Spass

and Setheo.

Solutions, questions and comments are welcomed by

ilf-serv-request@mathematik.hu-berlin.de

Ingo Dahn
dahn@uni-koblenz.de