  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.
