Advertisement

Soundness and Completeness Results II

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

Abstract

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.

Preview

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