UNIF'92 Program
Wednesday
| 09.00 - 09.30 | Announcements
|
Session 1 Semi-unification / AC
| 09.30 - 10.00 | Dennis Kfoury
| Type Reconstruction in Second Order Lambda Calculus
|
| 10.00 - 10.30 | Claude 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.00 | Tobias 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.05 | Hubert Comon
| Unification of Terms with Integer
Exponents
|
| 09.05 - 09.25 | Maribel Fernandez
| Negation Elimination in Equational
Formulae
|
| 09.25 - 09.45 | Denis 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.10 | Gert Smolka
| Relative Simplification: A Unifying
Priciple for Constraint Programming
|
| 11.10 - 11.40 | Ralf Treinen
| Relative Simplification for and
Independence of CFT
|
| 11.40 - 12.00 | Holzbauer
| Extensible Unification as Basis for the
Implementation of CLP Languages
|
Session 3 Features / Order-Sorted
| 13.30 - 14.00 | Hassan Ait-Kaci
| Order-Sorted Feature Theory Unification
|
| 14.00 - 14.30 | Bill Rounds
| Feature Algebras as Coalgebras:
A Category Perspective on Unification
|
| 14.30 - 14.50 | Rolf 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.00 | Klaus U. Schulz
| Combination Techniques and Decision
Problems for Disunification
|
| 16.00 - 16.30 | Zhenyu 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.30 | Evelyne 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
Other talks to be determined
Session 2 Applications
| 10.30 - 11.00 | Georgios Grivas
| A Unification- and Object-Based
Symbolic Computation System
|
| 11.00 - 11.20 | Mikael Rittri
| Retrieving Library Functions by Unifying
Types Modulo Linear Isomorphism
|
| 11.20 - 11.50 | Jü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.10 | Delia Kesner | Sequential Signatures
|
| 14.10 - 14.30 | Peter Baumgartner | Ordered Theory Resolution
|
[Past UNIF meetings]
[UNIF main page]
Ralf Treinen
November 24, 2000