Soundness and Completeness Results II
As in chapter 5, we will define a ground HE †-refutation method and then show the first-order version outlined in the previous chapter is sound and complete by appealing to the completeness of the ground method and the Skolen-Herbrand-Gödel theorem. The material on congruences associated with sets of Horn clauses was first developed by Gallier in , where he used it to define fast two algorithms which test the unsatisfiability of ground sets of Horn clauses with equality. It was subsequently used by Gallier and Raatz in  to define extensions of SLD-resolution via E-unification which admit logic programs with equality. We include it here because it will play a central role in showing the completeness of the equational extension to the Hornlog method.
Unable to display preview. Download preview PDF.