Soundness and Completeness Results I
Stan Raatz · Birkhäuser Boston eBooks · 1990
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.