Solving Equations Involving Sequence Variables and Sequence Functions - Artificial Intelligence and Symbolic Computation - page 157

Solving Equations Involving Sequence Variables
and Sequence Functions

Temur Kutsia

Research Institute for Symbolic Computation
Johannes Kepler University Linz
A-4040 Linz, Austria
[e-mail]

Abstract. Term equations involving individual and sequence variables,
and individual and sequence function symbols are studied. Function sym-
bols can have either fixed or flexible arity. A new unification procedure for
solving such equations is presented. Decidability of unification is proved.
Completeness and almost minimality of the procedure is shown.

1 Introduction

We study term equations with sequence variables and sequence function sym-
bols. A sequence variable can be instantiated by any finite sequence of terms,
including the empty sequence. A sequence function abbreviates a finite sequence
of functions all having the same argument lists 1 . An instance of such a function is
IntegerDivision(x,y) that abbreviates the sequence Quotient ( x , y ) , Remainder ( x , y ).
Bringing sequence functions in the language naturally allows Skolemization
over sequence variables: Let x, y be individual variables, x be a sequence variable,
and p be a flexible arity predicate symbol. Then

∀ x ∀ y ∃ x.p ( x, y, x ) Skolemizes to

∀ y.p ( x, y, f ( x, y )), where f is a binary Skolem sequence function symbol. An-

other example,

x ∀

x.p ( y, x ), where y is a sequence variable, after Skolemization
introduces a flexible arity sequence function symbol g :

∀ y ∃

y.p ( y, g ( y )).
Equation solving with sequence variables plays an important role in various
applications in automated reasoning, artificial intelligence, and programming.
At the end of the paper we briefly review some of the works related to this topic.
We contribute to this area by introducing a new unification procedure for
solving equations in the free theory with individual and sequence variables, and
individual and sequence function symbols. Function symbols can have either
fixed or flexible arity. We prove that solvability of an equation is decidable in
such a theory, and provide a unification procedure that enumerates an almost
minimal complete set of solutions. The procedure terminates if the set is finite.
This work is an extension and refinement of our previous results [10].
We implemented the procedure (without the decision algorithm) in Mathe-
matica [18] on the base of a rule-based programming system ρ Log

∀

2 [13].

Supported by the Austrian Science Foundation (FWF) under Project SFB F1302.
1 Semantically, sequence functions can be interpreted as multi-valued functions.
2 Available from http://www.ricam.oeaw.ac.at/people/page/marin/RhoLog/ .