From: PEM moderator
To:
Date: Wed, 23 Apr 2003 23:43:43 +0200
Subject: PEM meeting | 24.04.03 | CANCELLED

Precedence: bulk
X-url: http://www.cwi.nl/~pem

Mime-Version: 1.0
Content-Type: text/plain

   ****CANCELLED****

   Dear colleagues,

   Again,  some  virus  prohibits  a speaker from presenting his work. We
   wish  him  well,  and  hope the next PEM will not be challenged by the
   next virus!

   This announcement can be found at <http://www.cwi.nl/~pem>

         First-order Theorem Proving with Equality by Superposition

   Date:    24.04.03
   Time:    10:00
   Venue:   CANCELLED
   Speaker: Jürgen Stuber
   Title:   First-order Theorem Proving with Equality by Superposition

   We   give   an  introduction  to  superposition  theorem  proving  for
   first-order  logic  with  equality  and  some of its applications. The
   superposition  calculus  may  be  regarded  as a generalization of the
   Knuth-Bendix  completion  procedure for term rewriting systems to full
   first-order  clauses.  It is currently the state-of-the-art method for
   reasoning   in   first-order   logic   with   equality.  Its  ordering
   restrictions  and  strong  redundancy criteria in general cut down the
   search  space,  and  allow  to  use  superposition provers as decision
   procedures, e.g. the guarded fragment, modal and description logics.

   In  certain theories that contain a lot of equivalences, in particular
   set  theory, the need to transform the problem into clause normal form
   to  feed  the  prover  poses  problems,  as  it increases the size and
   obscures  the logical structure. We present a variant of superposition
   that   delays   the   clause   normal  form  transformation  and  uses
   equivalences  for directly rewriting logical formulas (joint work with
   Harald  Ganzinger,  MPI  Saarbrücken).  This allows a slow prover like
   Saturate  to  compete  on  set theory problems with the currently best
   provers  (Vampire, E-Setheo), which are at least an order of magnitude
   faster.
     _________________________________________________________________

   The  programming environment meetings are a forum for the presentation
   and  discussion  of  new  ideas,  ongoing and finished work. A typical
   meeting  addresses  a subject in the area of programming environments,
   program  generation, algebraic specification, term rewriting, parsing,
   etc.  A presentation ideally takes between 45 and 90 minutes. Meetings
   taking  longer  than 45 minutes are interrupted by a coffeebreak. Most
   Thursdays,  a  meeting is held which starts at 10:00 am. in one of the
   rooms at CWI/WINS. Exceptionally, dates or times may change.

   The    program    of    the    meetings    is    available   on   WWW:
   http://www.cwi.nl/~pem
     _________________________________________________________________