Conjunctive Queries, Existentially Quantified Systems of Equations and Finite Substitutions

TL;DR

This paper develops an elementary unification theory for positive conjunctive queries, introducing algorithms and lattice structures that relate formulas, substitutions, and systems of equations, with implications for logic programming.

Contribution

It presents a new unification algorithm for conjunctive queries, explores lattice-theoretic properties, and establishes an isomorphism between lattices of formulas and substitutions.

Findings

Algorithm for transforming conjunctive queries into solved form

Lattice of $ ext{E}$-formulas is complete and well-structured

Lattices of formulas and finite substitutions are isomorphic

Abstract

This report presents an elementary theory of unification for positive conjunctive queries. A positive conjunctive query is a formula constructed from propositional constants, equations and atoms using the conjunction $\wedge$ and the existential quantifier $\exists$. In particular, empty queries correspond to existentially quantified systems of equations -- called $\cal E$-formulas. We provide an algorithm which transforms any conjunctive query into a solved form. We prove some lattice-theoretic properties of queries. In particular, the quotient set of $\cal E$-formulas under an equivalence relation forms a complete lattice. Then we present another lattice -- a lattice of finite substitutions. We prove that the both lattices are isomorphic. Finally, we introduce the notion of application of substitutions to formulas and clarify its relationship to $\cal E$-formulas. This theory can be regarded as a basis for alternative presentation of logic programming.