2022/07/18 by Komara, Ján
#FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Programming Languages (cs.PL)
paper · doi:10.48550/arxiv.2207.08572
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 ∃. 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.