UNIF on Thursday

Detailed program
Thursday July 25th, 2002
See also the unified by-slot program


All sessions take place in auditorium 8.

Session 1

09:25-09:30  Welcome

09:30-10:30  Michael Kohlhase, Carnegie Mellon U, USA
Invited talk: Sorted higher-order unification
In recent years, many theorem proving systems have been extended to higher-order logic (in particular based on variants of the simply typed lambda calculus), not the least, since the built-in notion of beta-eta reduction gives a convenient and transparent definition mechanism. The drawback of this approach is that the main computational device (higher-order unification, which is undecidable in general), becomes a major bottleneck.
The main assumption in this talk is that the introduction of additional knowledge into higher-order unification will make the search for higher-order unifiers (and thus for proofs in higher-order logic) more guided and ultimately yield more efficient higher-order theorem provers. The source of knowledge that we want to explore in this talk is taxonomic information given in a concept hierarchy.
Concretely, we will introduce a sorted lambda-calculus where the universe is subdivided into various subsets (called sorts), and the signature is augmented by sort information. We introduce the technical device of term declarations, which give a very expressive mechanism for specifying (and using) sort information.
The central result will be a unification algorithm for this logic and some decidability results for the higher-order pattern fragment.
We will conclude the talk with a brief presentation of two applications of sorted higher-order unification outside theorem proving: natural language semantics and formula retrieval from knowledge bases.

Session 2

11:00-11:30  Manfred Schmidt-Schauß, Frankfurt U, Germany
Klaus U. Schulz, U Munich, Germany
Decidability of bounded higher-order unification
Unifiability of terms in the simply typed lambda calculus with β and η rules becomes decidable if there is a bound on the number of bound variables and lambdas in a unifier in η-long β-normal form.

11:30-12:00  Makoto Hamana, U Gunma, Japan
Simple β0-unification for terms with context holes

12:00-12:30  Joachim Niehren, Saarland U, Germany
Mateu Villaret, U Girona, Spain
Parallelism and tree regular constraints
Parallelism constraints are logical descriptions of trees. Parallelism constraints subsume dominance constraints and are equally expressive to context unification. Parallelism constraints belong to the constraint language for lambda structures (CLLS) which serves for modeling natural language semantics. In this paper, we investigate the extension of parallelism constraints by tree regular constraints. This canonical extension is subsumed by the monadic second-order logic over parallelism constraints. We analyze the precise expressiveness of this extension on basis of a new relationship between tree automata and logic. Our result is relevant for classifying different extensions of parallelism constraints, as in CLLS. Finally, we prove that parallelism constraints and context unification remain equivalent when extended with tree regular constraints.

Session 3

14:00-14:30  Benjamin Monate, U Paris XI (Paris-Sud), France
Parameterized string rewriting systems
We propose a new formalism for rewriting in order to describe infinite families of constrained string rewriting systems: parameterized string rewriting. Moreover, these systems may include parametric exponents or finite products. Our main result is a critical pair lemma allowing decision of local confluence. We apply this procedure to check automatically local confluence of parameterized rewriting presentations of some well-known families of monoids and groups.

14:30-15:00  Hitoshi Ohsaki, AIST, Japan
Toshinori Takai, AIST, Japan
A tree automata theory for unification modulo equational rewriting
An extension of the tree automata framework, called equational tree automata, is presented. This theory is useful to deal with unification modulo equational rewriting. We demonstrate how equational tree automata can be applied to unification problems.

15:00-15:30  Silvio Ghilardi, U Milan, Italy
Lorenzo Sacchetti, U Milan, Italy
Filtering unification: the case of modal logic
We deal with the case in which E-unification is filtering: this means that, given two solutions to a unification problem, there is always another one which is better than both of them. In this quite curious situation, unification problems can either be very nice (i.e. they admit a most general unifier), or extremely bad (no bases of unifiers exist). Examples are well-known: we have the commutative/monoidal theories. Commutative/monoidal theories include the [],∧,T-fragment of the system K. We shall show in this paper that filtering unification is quite common indeed in full modal systems. First of all, we prove that (under mild hypotheses) filtering unification is characterized by the fact that finitely presented projective algebras are closed under binary products. Secondly, we apply this characterization to the case of normal extensions E of the modal system K4 and show that E has filtering unification iff it extends K4.2+. There are extensions of K4.2+ for which most general unifiers do not exist, however they exist for systems like K4.2+, S4.2, GL.2+, Grz.2, etc.