| | All
sessions take place in auditorium 8.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. |
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. |
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 *K*4 and show that *E*
has filtering unification iff it extends *K*4.2^{+}. There
are extensions of *K*4.2^{+} for which most general
unifiers do not exist, however they exist for systems like *K*4.2^{+}, *S*4.2, *GL*.2^{+},
*Grz*.2, etc. |
| |