UNIF program

All sessions take place in auditorium 8.

Thursday July 25th

Thursday's program is also available with abstracts or side by side with other meetings.

09:25-10:30  Session 1

09:25  Welcome
09:30  Michael Kohlhase, Carnegie Mellon U, USA
Invited talk: Sorted higher-order unification

10:30-11:00  Refreshments

11:00-12:30  Session 2

11:00  Manfred Schmidt-Schauß, Frankfurt U, Germany and Klaus U. Schulz, U Munich, Germany
Decidability of bounded higher-order unification
11:30  Makoto Hamana, U Gunma, Japan
Simple β0-unification for terms with context holes
12:00  Joachim Niehren, Saarland U, Germany and Mateu Villaret, U Girona, Spain
Parallelism and tree regular constraints

12:30-14:00  Lunch

14:00-15:30  Session 3

14:00  Benjamin Monate, U Paris XI (Paris-Sud), France
Parameterized string rewriting systems
14:30  Hitoshi Ohsaki and Toshinori Takai, AIST, Japan
A tree automata theory for unification modulo equational rewriting
15:00  Silvio Ghilardi and Lorenzo Sacchetti, U Milan, Italy
Filtering unification: the case of modal logic

Friday July 26th

Friday's program is also available with abstracts or side by side with other meetings.

09:00-10:30  Session 4

09:00  Nachum Dershowitz, Tel Aviv U, Israel and Claude Kirchner, LORIA Nancy, France
Invited talk: Abstract canonical inference systems
10:00  Silvio Ranise, LORIA Nancy, France
A superposition decision procedure for the logic of equality with interpreted and uninterpreted functions

10:30-11:00  Refreshments

11:00-12:30  Session 5

11:00  Leo Bachmair, State U of New York-Stony Brook, USA and Christelle Scharff, Pace U, USA
Direct combination of completion and congruence closure
11:30  Mircea Marin and Aart Middeldorp, U Tsukuba, Japan
New completeness results for lazy conditional narrowing
12:00  Konstantin Korovin and Andrei Voronkov, U Manchester, UK
The decidability of the first-order theory of the Knuth-Bendix orders in the case of unary signatures

12:30-14:00  Lunch

14:00-15:30  Session 6

14:00  Christopher Lynch, Clarkson U, USA
Invited talk: Decidability and complexity of e-unification for some classes of equational theories
15:00  Siva Anantharaman, U Orléans, France; Paliath Narendran, State U of New York-Albany, USA; and Michaël Rusinowitch, LORIA Nancy, France
ACID-unification, rewrite reachability and set constraints

15:30-16:00  Refreshments

16:00-17:45  Session 7

16:00  Franz Baader, Dresden U of Techn., Germany and Cesare Tinelli, U Iowa, USA
ACU-unification with a successor symbol
16:30  Quang Huy Nguyen, LORIA Nancy, France
A constructive decision procedure for equalities modulo AC
17:00  Iliano Cervesato, ITT Industries, USA
Solution count for multiset unification with trailing multiset variables
17:30  Business Meeting