Conjunctive Queries, Existentially Quantified Systems of Equations and Finite Substitutions

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.