🚀 go-pugleaf

From: Hans-Juergen Buerckert <buerkert@informatik.uni-kl.de>
To: mod-ki@unido.informatik.uni-dortmund.de
Date: Thu, 26 Apr 90 13:34:50 MET DST
Subject: Ergaenzung zu CADE-10 Infos (mod-ki 427)
Keywords: Konferenzen

mod-ki message 0447
************************************************************************
CADE-10  Tutorial H

H: 15:30--18:00 Rewriting-Based Theorem Proving

Authors:
Jieh Hsiang, State University of New York at Stony Brook, USA, and
Jean-Pierre Jouannaud, Universite' de Paris-Sud a` Orsay, FRANCE.
 
Abstract:
Theorem proving involving equality has been one  of  the  most  exciting
research areas in automated deduction.  Wos and  Robinson  proposed  the
inference rule paramodulation and its refinement demodulation  in  1967.
At about the same time, Knuth and Bendix presented the  method  of  term
rewriting.  Term rewriting orients equations  into  rules  according  to
a well-founded ordering and selects the  deductive  consequences  via  a
notion of superposition.

In addition to equational theories, term rewriting has been successfully
extended to inductive theories, first order  logic,  first  order  logic
with  equality,  as  well  as  been  applied  to  functional and   logic
programming. In fact, it has already become one of the most  active  and
versatile areas in automated deduction.

In this tutorial, we introduce term rewriting  and  survey  its  diverse
applications.  We shall emphasize on the more  recent  developments  and
point  out  the  most  promising  approaches  as  well  as  some  future
directions of research.  We shall also present a unified  view  of  term
rewriting and paramodulation/demodulation.
************************************************************************