Soundness and Completeness Results II
Stan Raatz · Birkhäuser Boston eBooks · 1990
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 [24], 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 [29] 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.