Affiliations: Università di Verona, dovier@sci.univr.it | Università, di Udine, policrit@dimi.uniud.it | Università di Parma, gianfr@prmat.math.unipr.it
Note: [] Address for correspondence: Dipartimento Scientifico-Tecnologico, Universit` di Verona, Strada Le Grazie, 37134, Verona, Italy.
Note: [] Address for correspondence: Dipartimento di Matematica e Informatica, Università di Udine, Via delle Scienze 206, 33100, Udine, Italy.
Note: [] Address for correspondence: Dipartimento di Matematica, Universit` di Parma, Via M. D'Azeglio 85/A, 43100 Parma, Italy.
Abstract: The first-order theories of lists, multisets, compact lists (i.e., lists where the number of contiguous occurrences of each element is immaterial), and sets are introduced via axioms. Such axiomatizations are shown to be very well-suited for the integration with free functor symbols governed by the classical Clark's axioms in the context of (Constraint) Logic Programming. Adaptations of the extensionality principle to the various theories taken into account is then exploited in the design of unification algorithms for the considered data structures. All the theories presented can be combined providing frameworks to deal with several of the proposed data structures simultaneously. The unification algorithms proposed can be combined (merged) as well, to produce engines for such combination theories.
