A proof procedure for the logic of hereditary Harrop formulas (Q1311397): Difference between revisions

The basis for logic programming has traditionally been provided by the logic of Horn clauses. The simplicity of this logic, nevertheless, prevents the natural realization of several features considered important in modern programming languages. This fact has led to an interest in describing richer logics that, on the one hand, preserve the features of Horn clause logic that are important to their programming use and, on the other hand, provide a means for realizing additional desirable features. A logic that has been proposed in this regard is that of hereditary Harrop formulas. These formulas constitute an abstract logic programming language in some sense. The author presents a proof procedure for the logic of hereditary Harrop formulas. Proof search in intuitionistic logic is complicated by the nonexistence of a Herbrand-like theorem: formulas cannot be preprocessed into a clausal form and the construction of a proof is often sensitive to the order in which the connectives and quantifiers are analyzed. The considered formulas are examples of formulas for which a simple search procedure can be used. The proof procedure which is presented has a practical value in that it provides the basis for an implementation of the logic programming language \(\lambda\)-Prolog. Soundness and completeness of the proof procedure is provided. The author also presents the expansion of the procedure to higher-order hereditary Harrop formulas.