Deep Learning techniques are nowadays pervasive in AI. However, these approaches suffer from a lack of transparency for justifying their output and for helping users in believing in their decisions. For these reasons alternative approaches to learning deserve to be explored either for developing new tools with autonomous learning capability or for explaining the results of black-box predictors. Among them an important role is assumed since the Nineties by Inductive Logic Programming and, in particular, recently by the approaches of Learning from Answer Sets (LAS). Computing inductive solutions for LAS tasks is known to be Sigma P2 hard. In this work, we tackle this problem using a single-shot disjunctive ASP encoding based on the saturation technique originally proposed by Eiter and Gottlob. We prove that, when the background knowledge and hypothesis space form a tight program (a syntactical property) our encoding is linear in the size of the task. This approach contrasts with the state-of-the-art ILASP system, which relies on multiple iterative calls to an ASP solver. As a result, it can be directly evaluated by modern disjunctive ASP solvers, leveraging decades of research and optimization in the ASP community. We implement our method in a system named LASCO. Experimental results on a diverse set of benchmarks demonstrate that LASCO outperforms all versions of ILASP on many instances and it scales if run on multi-threaded machines.

Abstract Constraint Programming developed within Logic Programming in the Eighties; nowadays all Prolog systems encompass modules capable of handling constraint programming on finite domains demanding their solution to a constraint solver. This work focuses on a specific form of constraint, the so-called table constraint, used to specify conditions on the values of variables as an enumeration of alternative options. Since every condition on a set of finite domain variables can be ultimately expressed as a finite set of cases, Table can, in principle, simulate any other constraint. These characteristics make Table one of the most studied constraints ever, leading to a series of increasingly efficient propagation algorithms. Despite this, it is not uncommon to encounter real-world problems with hundreds or thousands of valid cases that are simply too many to be handled effectively with standard CPU-based approaches. In this paper, we deal with the Compact-Table (CT) algorithm, the state-of-the-art propagation algorithms for Table. We describe how CT can be enhanced by exploiting the massive computational power offered by modern Graphics Processing Units (GPUs) to handle large Table constraints. In particular, we report on the design and implementation of GPU-accelerated CT, on its integration into an existing constraint solver, and on an experimental validation performed on a significant set of instances.

This special issue of The Journal of Logic and Computation contains the revised and improved versions of selected papers presented at CILC-2023, the 38th Italian Conference on Computational Logic, which took place in Udine, Italy, from 21 to 23 June 2023. The Italian Association for Logic Programming (GULP) and the Department of Mathematics, Informatics and Physics of the University of Udine collaborated to organize this event. The yearly conferences of the Italian Association of Logic Programming, starting from 1986, have consistently offered valuable and inspiring opportunities for national and international researchers to share scientific findings, discuss ideas and suggest novel initiatives and projects in the field of Computational Logic. The continuous achievements of these conferences demonstrate the lively condition of a productive research field that addresses the theoretical foundations of logic programming and computational logics, the implementation techniques of logic programming languages and automated reasoning systems and the practical applications of the field.

Abstract The continuous interest in Artificial Intelligence (AI) has brought, among other things, the development of several scenarios where multiple artificial entities interact with each other. As for all the other autonomous settings, these multi-agent systems require orchestration. This is, generally, achieved through techniques derived from the vast field of Automated Planning. Notably, arbitration in multi-agent domains is not only tasked with regulating how the agents act, but must also consider the interactions between the agents’ information flows and must, therefore, reason on an epistemic level. This brings a substantial overhead that often diminishes the reasoning process’s usability in real-world situations. To address this problem, we present ECHO, a hierarchical framework that embeds classical and multi-agent epistemic (epistemic, for brevity) planners in a single architecture. The idea is to combine (i) classical; and(ii) epistemic solvers to model efficiently the agents’ interactions with the (i) ‘physical world’; and(ii) information flows, respectively. In particular, the presented architecture starts by planning on the ‘epistemic level’, with a high level of abstraction, focusing only on the information flows. Then it refines the planning process, due to the classical planner, to fully characterize the interactions with the ‘physical’ world. To further optimize the solving process, we introduced the concept of macros in epistemic planning and enriched the ‘classical’ part of the domain with goal-networks. Finally, we evaluated our approach in an actual robotic environment showing that our architecture indeed reduces the overall computational time.

Abstract The AllDifferent constraint is a fundamental tool in Constraint Programming. It naturally arises in many problems, from puzzles to scheduling and routing applications. Such popularity has prompted an extensive literature on filtering and propagation for this constraint. This paper investigates the use of General Processing Units (GPUs) to accelerate filtering and propagation. In particular, the paper presents an efficient parallelization of the AllDifferent constraint on GPU, along with an analysis of different design and implementation choices and evaluation of the performance of the resulting system on several benchmarks.

Abstract In this paper, we analyze the physical puzzle IcoSoKu, a game about placing some given triangular tiles on the faces of an icosahedron in order to fill the capacities of its vertices, and we propose its generalization called 3coSoKu, admitting an arbitrary playing field with triangular faces, arbitrary capacities and an arbitrary set of triangular tiles. First, we prove the strong NP-completeness of 3coSoKu, even when the playing field is a convex polyhedron with equilateral triangles as faces. Second, we encode 3coSoKu both in the constraint modeling language MiniZinc and in the logic programming paradigm known as Answer Set Programming and we develop a visual tool for an accessible interface to the solver. Finally, we use our encodings to verify experimentally that every initial state for IcoSoKu admits a solution.

Abstract Multi-core and highly connected architectures have become ubiquitous, and this has brought renewed interest in language-based approaches to the exploitation of parallelism. Since its inception, logic programming has been recognized as a programming paradigm with great potential for automated exploitation of parallelism. The comprehensive survey of the first twenty years of research in parallel logic programming, published in 2001, has served since as a fundamental reference to researchers and developers. The contents are quite valid today, but at the same time the field has continued evolving at a fast pace in the years that have followed. Many of these achievements and ongoing research have been driven by the rapid pace of technological innovation, that has led to advances such as very large clusters, the wide diffusion of multi-core processors, the game-changing role of general-purpose graphic processing units, and the ubiquitous adoption of cloud computing. This has been paralleled by significant advances within logic programming, such as tabling, more powerful static analysis and verification, the rapid growth of Answer Set Programming, and in general, more mature implementations and systems. This survey provides a review of the research in parallel logic programming covering the period since 2001, thus providing a natural continuation of the previous survey. In order to keep the survey self-contained, it restricts its attention to parallelization of the major logic programming languages (Prolog, Datalog, Answer Set Programming) and with an emphasis on automated parallelization and preservation of the sequential observable semantics of such languages. The goal of the survey is to serve not only as a reference for researchers and developers of logic programming systems but also as engaging reading for anyone interested in logic and as a useful source for researchers in parallel systems outside logic programming.

The main goal of this work is to propose a tool-chain capable of analyzing a data collection of temporally qualified (genetic) mutation profiles, i.e., a collection of DNA-sequences (genes) that present variations with respect to their “healthy” versions. We implemented a system consisting of a front-end, a reasoning core, and a post-processor: the first transforms the input data retrieved from medical databases into a set of logical facts, while the last displays the computation results as graphs. Concerning the reasoning core, we employed the Answer Set Programming paradigm, which is capable of deducing complex information from data. However, since the system is modular, this component can be replaced by any logic programming tool for different kinds of data analysis. Indeed, we tested the use of a probabilistic inductive logic programming core.

Abstract Designing agents that reason and act upon the world has always been one of the main objectives of the Artificial Intelligence community. While for planning in “simple” domains the agents can solely rely on facts about the world, in several contexts,e.g., economy, security, justice and politics, the mere knowledge of the world could be insufficient to reach a desired goal. In these scenarios,epistemicreasoning,i.e., reasoning about agents’ beliefs about themselves and about other agents’ beliefs, is essential to design winning strategies. This paper addresses the problem of reasoning in multi-agent epistemic settings exploiting declarative programming techniques. In particular, the paper presents an actual implementation of a multi-shotAnswer Set Programming-based planner that can reason in multi-agent epistemic settings, called PLATO (ePistemic muLti-agentAnswer seTprogramming sOlver). The ASP paradigm enables a concise and elegant design of the planner, w.r.t. other imperative implementations, facilitating the development of formal verification of correctness. The paper shows how the planner, exploiting an ad-hoc epistemic state representation and the efficiency of ASP solvers, has competitive performance results on benchmarks collected from the literature.

In order to enable logic programming to deal with the diversity of pervasive systems, where many heterogeneous, domain-specific computational models could benefit from the power of symbolic computation, we explore the expressive power of labelled systems. To this end, we define a new notion of trut h for logic programs extended with labelled variables interpreted in non-Herbrand domains—where, however, terms maintain their usual Herbrand interpretations. First, a model for labelled variables in logic programming is defined. Then, the fixpoint and the operational semantics are presented and their equivalence is formally proved. A meta-interpreter implementing the operational semantics is also introduced, followed by some case studies aimed at showing the effectiveness of our approach in selected scenarios.

The multiple-origin-multiple-destination (MOMD) problem is a simplified version of the logistics planning problem in which packages are required to be transported from their origins to their destinations by multiple trucks with a minimum total cost. This paper proves the NP-hardness of the problem and gives two constraint models for solving the problem optimally. These models are then solved by SAT and MIP solvers (after some translation) and the results are experimentally compared with ASP and CP problem encodings.

This paper explores the use of Binary Decision Diagrams (BDDs) in Conformant Planning. A conformant planner, called BPA, based on the BDD representation for belief sets is developed. Heuristics that fit with the BDD representation are presented and analyzed experimentally. The paper confirms the strong potential of BDDs to enhance performance of heuristic search based conformant planners.

Current research in planning focuses mainly on so called domain independent models using the Planning Domain Description Language (PDDL) as the domain modeling language. This declarative modeling approach embraces the idea of a physics-only model describing how actions change the world. However, PDDL omits information about why and when the actions should be applied to reach the goal, which significantly decreases the practical applicability of PDDL. There exist approaches such as Hierarchical Task Networks (HTN) and control rules that add this type of information to the model with the pay-off of increased efficiency but also with the downside of increased complexity and code sizes.

In this paper we study the semantics of Coinductive Logic Programming and clarify its intrinsic computational limits, which prevent, in particular, the definition of a complete, computable, operational semantics. We propose a new operational semantics that allows a simple correctness result and the definition of a simple meta-interpreter. We compare, and prove the equivalence, with the operational semantics defined and used in other papers on this topic.

This paper provides a novel perspective in the protein structure prediction (PSP) problem. The PSP problem focuses on determining putative 3D structures of a protein starting from its primary sequence. The proposed approach relies on a multi-agent system (MAS) perspective, where concurrent agents explore the folding of different parts of a protein. The strength of the approach lies in the agents’ ability to apply different types of knowledge, expressed in the form of declarative constraints, to prune the search space of folding alternatives. The paper makes also an important contribution in demonstrating the suitability of a general-purpose graphical processing unit approach to implement such MAS infrastructure, with significant performance improvements over the sequential implementation and other methods.

The parallel computing power offered by graphic processing units (GPUs) has been recently exploited to support general purpose applications – by exploiting the availability of general API and the single-instruction multiple-thread-style parallelism present in several classes of problems (e.g. numerical simulations and matrix manipulations) – where relatively simple computations need to be applied to all items in large sets of data. This paper investigates the use of GPUs in parallelising a class of search problems, where the combinatorial nature leads to large parallel tasks and relatively less natural symmetries. Specifically, the investigation focuses on the well-known satisfiability testing (SAT) problem and on the use of the NVIDIA compute unified device architecture, one of the most popular platforms for GPU computing. The paper explores ways to identify strong sources of GPU-style parallelism from SAT solving. The paper describes experiments with different design choices and evaluates the results. The outcomes demonstrate the potential for this approach, leading to one order of magnitude of speedup using a simple NVIDIA platform.

Abstract This paper describes Picat's planner, its implementation, and planning models for several domains used in International Planning Competition (IPC) 2014. Picat's planner is implemented by use of tabling. During search, every state encountered is tabled, and tabled states are used to effectively perform resource-bounded search. In Picat, structured data can be used to avoid enumerating all possible permutations of objects, and term sharing is used to avoid duplication of common state data. This paper presents several modeling techniques through the example models, ranging from designing state representations to facilitate data sharing and symmetry breaking, encoding actions with operations for efficient precondition checking and state updating, to incorporating domain knowledge and heuristics. Broadly, this paper demonstrates the effectiveness of tabled logic programming for planning, and argues the importance of modeling despite recent significant progress in domain-independent PDDL planners.

Constraint programming has gained prominence as an effective and declarative paradigm for modeling and solving complex combinatorial problems. Techniques based on local search have proved practical to solve real-world problems, providing a good compromise between optimality and efficiency. In spite of the natural presence of concurrency, there has been relatively limited effort to use novel massively parallel architectures, such as those found in modern Graphical Processing Units (GPUs), to speedup local search techniques in constraint programming. This paper describes a novel framework which exploits parallelism from a popular local search method (the Large Neighborhood Search method), using GPUs.

This paper provides a novel perspective in the Protein Structure Prediction (PSP) problem. The PSP problem focuses on determining putative 3D structures of a protein starting from its primary sequence. The proposed approach relies on a multi-agents approach, where concurrent agents explore the folding of different parts of a protein. The strength of the approach lies in the agents' ability to apply different types of knowledge (expressed in the form of declarative constraints) to prune the local space of folding alternatives. The paper demonstrates the suitability of a GPU approach to implement such multi-agent infrastructure, with significant improvements in speed and quality of solutions w.r.t. other methods (e.g., based on fragments assembly approaches).

This paper presents our program in B-Prolog submitted to the third ASP solver competition for the Sokoban problem. This program, based on dynamic programming, treats Sokoban as a generalized shortest path problem. It divides a problem into independent subproblems and uses mode-directed tabling to store subproblems and their answers. This program is very simple but quite efficient. Without use of any sophisticated domain knowledge, it easily solves 14 of the 15 instances used in the competition. We show that the approach can be easily applied to other optimization planning problems.

Abstract The paper presents a knowledge representation formalism, in the form of a high-levelAction Description Language (ADL)for multi-agent systems, where autonomous agents reason and act in a shared environment. Agents are autonomously pursuing individual goals, but are capable of interacting through a shared knowledge repository. In their interactions through shared portions of the world, the agents deal with problems of synchronization and concurrency; the action language allows the description of strategies to ensure a consistent global execution of the agents’ autonomously derived plans. A distributed planning problem is formalized by providing the declarative specifications of the portion of the problem pertaining to a single agent. Each of these specifications is executable by a stand-alone CLP-based planner. The coordination among agents exploits a Linda infrastructure. The proposal is validated in a prototype implementation developed in SICStus Prolog.

We are proud to introduce this special issue of the Journal of Theory and Practice of Logic Programming (TPLP), dedicated to the full papers accepted for the 28th International Conference on Logic Programming (ICLP). The ICLP meetings started in Marseille in 1982 and since then constitute the main venue for presenting and discussing work in the area of logic programming.

This paper presents our program in B-Prolog submitted to the third ASP solver competition for the Sokoban problem. This program, based on dynamic programming, treats Sokoban as a generalized shortest path problem. It divides a problem into independent sub problems and uses tabling to store sub problems and their answers. This program is very simple but quite efficient. Without use of any sophisticated domain knowledge, it easily solved 11 of the 15 instances used in the competition.

The paper investigates a novel approach, based on Constraint Logic Programming (CLP), to predict potential 3D conformations of a protein via fragments assembly. The fragments are extracted and clustered by a preprocessor from a database of known protein structures. Assembling fragments into a complete conformation is modeled as a constraint satisfaction problem solved using CLP. The approach makes use of a simplified Cα-side chain centroid protein model, that offers efficiency and a good approximation for space filling. The approach adapts existing energy models for protein representation and applies a large neighboring search (LNS) strategy. The results show the feasibility and efficiency of the method, and the declarative nature of the approach simplifies the introduction of additional knowledge and variations of the model.

Product configuration systems are an emerging software technology that supports companies in deploying mass customization strategies. In this paper, we describe a CLP-based reasoning engine that we developed for a commercial configuration system. We

This paper explores the use of Constraint Logic Programming (CLP) as a platform for experimenting with planning problems in the presence of multiple interacting agents. The paper develops a novel constraint-based action language, ℬMAP , that enables

Abstract Action description languages, such as and ℬ (Gelfond and Lifschitz,Electronic Transactions on Artificial Intelligence, 1998, vol. 2, pp. 193—210), are expressive instruments introduced for formalizing planning domains and planning problem instances. The paper starts by proposing a methodology to encode an action language (with conditional effects and static causal laws), a slight variation of ℬ, usingConstraint Logic Programming over Finite Domains. The approach is then generalized to raise the use of constraints to the level of the action language itself. A prototype implementation has been developed, and the preliminary results are presented and discussed.

Abstract The paper investigates a novel approach, based on Constraint Logic Programming (CLP), to predict the 3D conformation of a protein via fragments assembly. The fragments are extracted by a preprocessor—also developed for this work—from a database of known protein structures that clusters and classifies the fragments according to similarity and frequency. The problem of assembling fragments into a complete conformation is mapped to a constraint solving problem and solved using CLP. The constraint-based model uses a medium discretization degree Cα-side chain centroid protein model that offers efficiency and a good approximation for space filling. The approach and adapts existing energy models to the protein representation used and applies a large neighboring search strategy. The results shows the feasibility and efficiency of the method. The declarative nature of the solution allows to include future extensions, e.g., different size fragments for better accuracy.

In recent years, Answer Set Programming has gained popularity as a viable paradigm for applications in knowledge representation and reasoning. This paper presents a novel methodology to compute answer sets of an answer set program. The proposed methodology maintains a bottom-up approach to the computation of answer sets (as in existing systems), but it makes use of a novel structuring of the computation, that originates from the non-ground version of the program. Grounding is lazily performed during the computation of the answer sets. The implementation has been realized using Constraint Logic Programming over finite domains.

This paper presents experimental comparisons between the declarative encodings of various computationally hard problems in Answer Set Programming (ASP) and Constraint Logic Programming over Finite Domains (CLP(FD)). The objective is to investigate how solvers in the two domains respond to different problems, highlighting the strengths and weaknesses of their implementations, and suggesting criteria for choosing one approach over the other. Ultimately, the work in this paper is expected to lay the foundations for a transfer of technology between the two domains, for example by suggesting ways to use CLP(FD) in the execution of ASP.

Lists, multisets, and sets are well-known data structures whose usefulness is widely recognized in various areas of computer science. They have been analyzed from an axiomatic point of view with a parametric approach in Dovier et al. [1998], where the relevant unification algorithms have been developed. In this article, we extend these results considering more general constraints, namely, equality and membership constraints and their negative counterparts.

Abstract This paper presents the design, implementation and application of a constraint programming framework on 3D crystal lattices. The framework provides the flexibility to express and resolve constraints dealing with structural relationships of entities placed in a 3D lattice structure in space. Both sequential and parallel implementations of the framework are described, along with experiments that highlight its superior performance with respect to the use of more traditional frameworks (e.g. constraints on finite domains and integer programming) to model lattice constraints. The framework is motivated and applied to address the problem of solving the protein folding prediction problem, i.e. predicting the 3D structure of a protein from its primary amino acid sequence. Results and comparison with performance of other constraint‐based solutions to this problem are presented. Copyright © 2007 John Wiley & Sons, Ltd.

In this paper we demonstrate how Interval Analysis and Constraint Logic Programming can be used to obtain an accurate geometric model of a scene that rigorously takes into account the propagation of data errors and roundoff. Image points are represented as small rectangles: As a result, the output of the n-views triangulation is not a single point in space, but a polyhedron that contains all the possible solutions. Interval Analysis is used to bound this polyhedron with a box. Geometrical constraints such as orthogonality, parallelism, and coplanarity are subsequently enforced in order to reduce the size of those boxes, using Constraint Logic Programming. Experiments with real calibrated images illustrate the approach.

Formal set theory is traditionally concerned with pure sets; consequently, the satisfiability problem for fragments of set theory was most often addressed (and in many cases positively solved) in the pure framework. In practical applications, however, it is common to assume the existence of a number of primitive objects (sometimes called atoms ) that can be members of sets but behave differently from them. If these entities are assumed to be devoid of members, the standard extensionality axiom must be revised; then decidability results can sometimes be achieved via reduction to the pure case and sometimes can be based on direct goal-driven algorithms. An alternative approach to modeling atoms that allows one to retain the original formulation of extensionality was proposed by Quine: atoms are self-singletons. In this article we adopt this approach in coping with the satisfiability problem: We show the decidability of this problem relativized to ∃*∀-sentences, and develop a goal-driven unification algorithm.

The unification problem in algebras capable of describing sets has been tackled, directly or indirectly, by many researchers and it finds important applications in various research areas, e.g. deductive databases, theorem proving, static analysis, rapid software prototyping. The various solutions proposed are spread across a large literature. In this paper we provide a uniform presentation of unification of sets, formalizing it at the level of set theory. We address the problem of deciding existence of solutions at an abstract level. This provides also the ability to classify different types of set unification problems. Unification algorithms are uniformly proposed to solve the unification problem in each of such classes. The algorithms presented are partly drawn from the literature – and properly revisited and analyzed – and partly novel proposals. In particular, we present a new goal-driven algorithm for general unification.

The paper describes a constraint-based solution to the protein folding problem on face-centered cubic lattices---a biologically meaningful approximation of the general protein folding problem. The paper improves the results presented in [15] and introduces new ideas for improving efficiency: (i) proper reorganization of the constraint structure; (ii) development of novel, both general and problem-specific, heuristics; (iii) exploitation of parallelism. Globally, we obtain a speed up in the order of 60 w.r.t. [15]. We show how these results can be employed to solve the folding problem for large proteins containing subsequences whose conformation is already known.

BACKGROUND: The protein structure prediction problem is one of the most challenging problems in biological sciences. Many approaches have been proposed using database information and/or simplified protein models. The protein structure prediction problem can be cast in the form of an optimization problem. Notwithstanding its importance, the problem has very seldom been tackled by Constraint Logic Programming, a declarative programming paradigm suitable for solving combinatorial optimization problems. RESULTS: Constraint Logic Programming techniques have been applied to the protein structure prediction problem on the face-centered cube lattice model. Molecular dynamics techniques, endowed with the notion of constraint, have been also exploited. Even using a very simplified model, Constraint Logic Programming on the face-centered cube lattice model allowed us to obtain acceptable results for a few small proteins. As a test implementation their (known) secondary structure and the presence of disulfide bridges are used as constraints. Simplified structures obtained in this way have been converted to all atom models with plausible structure. Results have been compared with a similar approach using a well-established technique as molecular dynamics. CONCLUSIONS: The results obtained on small proteins show that Constraint Logic Programming techniques can be employed for studying protein simplified models, which can be converted into realistic all atom models. The advantage of Constraint Logic Programming over other, much more explored, methodologies, resides in the rapid software prototyping, in the easy way of encoding heuristics, and in exploiting all the advances made in this research area, e.g. in constraint propagation and its use for pruning the huge search space.

In this paper we propose a semantically well-founded combination of the constraint solvers used in the constraint programming languages CLP(SET) and CLP(FD). This work demonstrates that it is possible to provide efficient executions (through CLP(FD) solvers) while maintaining the expressive power and flexibility of the CLP(SET) language. We develop a combined constraint solver and we show how static analysis can help in organizing the distribution of constraints to the two constraint solvers.

We study the complexity of the Subgraph Bisimulation Problem, which relates to Graph Bisimulation as Subgraph Isomorphism relates to Graph Isomorphism, and we prove its NP-Completeness. Our analysis is motivated by its applications to semistructured databases.

Set Theory for Computing: From Decision Procedures to Declarative Programming with Sets by Domenico Cantone, Eugenio Omodeo and Alberto Policriti, Springer-Verlag, 2001. Hardback: ISBN 0-387-95197-0, 69.95, xviii+409 pages. - Volume 3 Issue 1

In this paper we present a study of the problem of handling constraints made by conjunctions of positive and negative literals based on the predicate symbols =, ∈,∪ and || (i.e., disjointness of two sets) in a (hybrid) universe of finite sets . We also review and compare the main techniques considered to represent finite sets in the context of logic languages. The resulting contraint algorithms are embedded in a Constraint Logic Programming (CLP) language which provides finite sets—along with basic set-theoretic operations—as first-class objects of the language. The language—called CLP( SET )—is an instance of the general CLP framework, and as such it inherits all the general features and theoretical results of this scheme. We provide, through programming examples, a taste of the expressive power offered by programming in CLP( SET ).

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.