Soundness and Completeness Results II

  • Stan Raatz
Part of the Progress in Computer Science and Applied Logic book series (PCS, volume 10)


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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Copyright information

© Springer Science+Business Media New York 1990

Authors and Affiliations

  • Stan Raatz
    • 1
  1. 1.Department of Computer ScienceRutgers UniversityNew BrunswickUSA

Personalised recommendations