[Prev][Next][Index][Thread]
*** FLOC-99 --- WORKSHOP AND CONTEST ON INDUCTIVE THEOREM PROVING ***
-
To: theorem-provers@ai.mit.edu, types@cis.upenn.edu, compunode@dfki.de, rewriting@ens-lyon.fr, logic@cs.cornell.edu, logic@theory.lcs.mit.edu, softverf@leopard.cs.byu.edu, amast@cs.utwente.nl, cs-logic@cs.indiana.edu, kgs@logic.tuwien.ac.at, lprolog@central.cis.upenn.edu, theorynt@listserv.nodak.edu, fg121@bach.informatik.uni-ulm.de, dreamers@dai.ed.ac.uk
-
Subject: *** FLOC-99 --- WORKSHOP AND CONTEST ON INDUCTIVE THEOREM PROVING ***
-
From: Dieter Hutter <hutter@dfki.de>
-
Date: Mon, 15 Mar 1999 11:28:25 +0100
-
Organization: DFKI Saarbruecken GmbH, D 66123 Saarbruecken
CALL FOR PAPERS, SYSTEMS AND PARTICIPATION:
-------------------------------------------
FLOC-99 WORKSHOP ON AUTOMATION OF PROOFS BY MATHEMATICAL INDUCTION
==================================================================
& CONTEST FOR INDUCTIVE THEOREM PROVERS
========================================
Proof by Mathematical Induction presents the Automated Deduction
community with some very challenging research problems. The aim
of this one day workshop is to create an informal forum in which
hot-topics and emerging techniques can be presented and discussed.
1. CONTEST:
-----------
Part of the workshop will be a contest for inductive theorem provers.
The contest will be mainly based on an edited list of over 2000 problem drawn
from the nqthm-92 release and converted into a sorted language. The contest
will be held offline before the workshop and due to the intrinsic complexity
of any standard of comparison there will be no official winner. Each team
will be expected to fill in a questionaire explaining their results, e.g
the rate of success, the rate of interactions, the time spent for each
example, the behaviour on non-provable examples etc.
Each team will be expected to run its system during the workshop. A sample
of examples will be arranged from the testbed and will be given to the
systems online during the workshop verifying the proposed results. More
information about the contest will be available at the home-page of the
workshop:
http://www.dfki.de/floc-ws13
Teams who are interested in joining the contest are encouraged to contact
hutter@dfki.de (Dieter Hutter (DFKI))
as soon as possible, by April, 1st, 1999.
2. PROGRAMME:
-------------
Besides the contest the workshop will feature invited talks and contributed
presentations with ample time for discussion regarding topics like:
application to formal methods, higher-order inductive theorem proving,
proof planning and proof strategies, challenging problems.
Consistent with the workshop format, we expect and encourage contributed
talks to present work in progress, rather than polished final results.
Attendance is by invitation only, based on the received submissions, but
we will consider late requests for participation. All workshop attendees
are expected to register for one of the main FLoC'99 conferences.
Authors interested in presenting their work related to the workshop are
invited to submit an extended abstract of up to 10 pages. Researchers
interested in attending the workshop without giving a talk may send a
position paper of 1-2 pages describing their interest in the mentioned
topics.
All submissions should be sent to
hutter@dfki.de (Dieter Hutter (DFKI))
in postscript format by April, 1st, 1999.
Accepted contributions will be included in the workshop proceedings which
will be available at the workshop and on the workshop web page.
ORGANIZING AND PROGRAMME COMMITTEE:
Dieter Hutter, DFKI GmbH, Saarbruecken
Alan Bundy, University of Edinburgh
Fausto Giunchiglia, IRST, Trento
Andrew Ireland, Heriott Watt University, Edinburgh