Agostino Dovier

Title: Agostino Dovier

Main Research Question: The paper aims to provide a uniform overview of the unification problem in algebras capable of describing sets.

Methodology: The authors present a new goal-driven algorithm for general ACI unification and a new algorithm with a simple termination proof for general (Ab)(Cℓ) unification.

Results: The paper covers all instances of the unification problem, providing a comprehensive analysis of different solutions. It presents a new algorithm for general ACI unification and proves its correctness and completeness, along with a termination proof.

Implications: This work contributes to the field by providing a first uniform presentation of the unification problem, surveying different solutions and offering new algorithms with promising properties. It can help advance research in various areas such as deductive databases, theorem proving, and static analysis.

Link to Article: https://arxiv.org/abs/0110023v1 Authors: arXiv ID: 0110023v1