UNIF'92 Program

Wednesday

09.00 - 09.30Announcements

Session 1 Semi-unification / AC

09.30 - 10.00Dennis Kfoury Type Reconstruction in Second Order Lambda Calculus
10.00 - 10.30Claude Kirchner Associative Commutative Matching Based on the Syntacticity of the AC Theory

Session 2 AC / AC1

10.45 - 11.15 Stefan Hölldobler AC1-Unification/Matching in Linear Logic Programming
11.15 - 11.45 Martin Henz Integrating AC1-unification into the Process of Completion modulo AC1
11.45 - 12.00 Announcement of System Demos

Session 3 General E-Unification / Narrowing

13.30 - 14.00 Erik Hamoen Counterexamples to Completeness Results for Basic Narrowing
14.00 - 14.30 Stefan Kurtz Narrowing and Basic Forward Closures
14.30 - 15.00 Bertrand Delsart Conditional Rewriting Presentations for General E-Unification

Session 4 Higher-Order

15.30 - 16.00Tobias Nipkow Efficient Unification of Higher-Order Patterns
16.00 - 16.30 Franz Weber Minimal and Complete Higher Order E-Unification
16.30 - 16.50 Ullrich Hustadt A Complete Transformation System for Polymorphic Higher-Order Unification
16.50 - 17.10 Marian Vittek A Combinatory Logic Rewriting Relation Which Supports Narrowing
17.10 - 17.30 David Wolfram The Decidability of Higher-Order Matching

19.30 - 20.30 System Demos
20.30 - 21.00 Business Meeting

Thursday

Session 1 Generalizations of Unification

08.45 - 09.05Hubert Comon Unification of Terms with Integer Exponents
09.05 - 09.25Maribel Fernandez Negation Elimination in Equational Formulae
09.25 - 09.45Denis Lugiez Complement Problems and Tree Automata
09.45 - 10.05 Toby Walsh Difference Matching
10.05 - 10.25 Jörg Würtz Unifying Cycles

Session 2 Constraints

10.40 - 11.10Gert Smolka Relative Simplification: A Unifying Priciple for Constraint Programming
11.10 - 11.40Ralf Treinen Relative Simplification for and Independence of CFT
11.40 - 12.00Holzbauer Extensible Unification as Basis for the Implementation of CLP Languages

Session 3 Features / Order-Sorted

13.30 - 14.00Hassan Ait-Kaci Order-Sorted Feature Theory Unification
14.00 - 14.30Bill Rounds Feature Algebras as Coalgebras: A Category Perspective on Unification
14.30 - 14.50Rolf Backofen A Complete and Decidable Feature Theory
14.50 - 15.10 Werner On Approaches to Order-Sorted Rewriting

Session 4 Combination / Specific Theories

15.40 - 16.00Klaus U. Schulz Combination Techniques and Decision Problems for Disunification
16.00 - 16.30Zhenyu Qian Higher-Order E-Unification for Arbitrary Theories
16.30 - 17.00 Christophe Ringeissen Unification in a Combination of Equational Theories with shared Constants and its Application to Primal Algebras
17.00 - 17.30Evelyne Contejean Unification Problems Modulo Distributivity

19.30 - 21.00 Panel Discussion Ait-Kaci, Comon, Jouannaud, Kfoury, Kirchner, Rounds, Siekmann, Smolka

Friday

Session 1 Complexity / to be determined

08.45 - 09.15Paliath Narendran Complexity of E-Unification Problems
Other talks to be determined

Session 2 Applications

10.30 - 11.00Georgios Grivas A Unification- and Object-Based Symbolic Computation System
11.00 - 11.20Mikael Rittri Retrieving Library Functions by Unifying Types Modulo Linear Isomorphism
11.20 - 11.50Jürgen Avenhaus Conditional Rewriting modulo a Built-in Algebra

Session 3 Miscellaneous

13.30 - 13.50 Leszek Pacholski Undecidability of the Horn-clause Implication Problem
13.50 - 14.10Delia KesnerSequential Signatures
14.10 - 14.30Peter BaumgartnerOrdered Theory Resolution


[Past UNIF meetings] [UNIF main page]
Ralf Treinen
November 24, 2000