Soundness and Completeness Results I

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


In this chapter we will show that the Hornlog proof method is sound and complete, and that it enjoys the adequacy property defined in chapter 3. We will follow the following guideline in showing these results. First, the method in the ground case is presented and proved complete. Then first-order extension outlined in the previous chapter is shown to be complete by appealing to the completeness of the ground case and the Skolem-Herbrand-Gödel theorem. Finally, the soundness and completeness of the method as a computational procedure is established by showing that the set of substitutions returned exactly coincides with the model-theoretic semantics defined for the language. This methodology is particularly appropriate for logic programming because it yields a lifting lemma which constructively illustrates the relationship between the ground and first-order cases.


Logic Program Completeness Result Horn Clause Denotational Semantic Expansion Step 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


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