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 $\mathrm{\exists }$. In particular, empty queries correspond to existentially quantified systems of equations – called $\mathcal{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 $\mathcal{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 $\mathcal{E}$-formulas. This theory can be regarded as a basis for alternative presentation of logic programming.