This workshop takes place on Tuesday, 30 July 1996, in conjunction with the CADE-13 conference at Rutgers University (New Brunswick, New Jersey, USA). It is organized by Miki Hermann (CRIN(CNRS)&INRIA-Lorraine, Nancy) and Gernot Salzer (Technische Universität Wien, Vienna).
Below you find:
A common phenomenon throughout all areas dealing with first order terms (particularly in automated deduction) are infinite sequences of structurally similar terms. One characteristic of computer science is its emphasis on finite structures. Consequently, various formalisms and methods have been proposed to capture these sequences by finite means, among them schematizations of terms.
A schematization is a finite expression together with a mechanism for effectively generating the elements of the set. In addition, it should be possible to compute the unifying intersection of infinite term sets by manipulating their finite schematizations.
The aim of the workshop is to bring together researchers working on schematizations and to discuss the different approaches as well as their applications in clausal theorem proving, term rewriting, unification theory, finite model building, and other areas.
Topics of interest include, but are not restricted to:
For a detailed description of the topic see the workshop proposal.
Gernot Salzer
Technische Universität Wien
Karlsplatz 13/E185-2
A-1040 Wien, Austria
Phone: (+43 1) 588 01 4096
Fax: (+43 1) 504 15 89
E-mail: schema@logic.at