Extending Horn clause logic with implication goals (Q1186427)

Since the mid of the eighties the problem of structuring logic programs received a stronger attention in the logic programming community. In the spirit of this problem, the authors define an extension of Horn logic based on the concept of implication goals. Not only Horn clauses of the type \(G_ 1\wedge\dots\wedge G_ n\to A\) are allowed for atomic \(G_ i\), but the \(G_ i\) may have the form \(D\supset G\), where \(D\) is a set of clauses (representing local declarations) and \(G\) is a goal in the usual sense. In this language two different concepts of implications have to be considered: ``\(\to\)'', the usual implication and ``\(\supset\)'' the implication in goals. Conceptually the paper is based on the paradigm of open blocks with static scope rules. The scopes of the blocks are defined by variable quantification by which local and global variables can be distinguished. Formally goals \((\langle G\rangle)\) and definite clauses \((\langle DC\rangle)\) are defined as: \[ \begin{aligned} \langle G\rangle & \Rightarrow \text{TRUE}|\langle\text{Atom}\rangle|\langle G\rangle\wedge\langle G\rangle|\exists x\langle G\rangle|\langle DC\rangle\supset\langle G\rangle, \\ \langle DC\rangle & \Rightarrow\langle G\rangle\to\langle\text{Atom}\rangle |\langle DC\rangle\wedge\langle DC\rangle|(\forall x)\langle DC\rangle.\end{aligned} \] As in Horn logic, a program is defined as a set of definite clauses. The authors introduce an operational semantics which is defined on lists of the form \(P_ 1|\dots| P_ n\), where the \(P_ i\) are programs and the \('\mid '\) represents a block nesting. The operational semantics is based on a kind of linear input deduction, but is defined via ground instantiation. Additionally a fixpoint semantics and a model theoretic semantics are introduced and the soundness and completeness of all concepts w.r.t. each other is demonstrated. In the model theoretic semantics, \(\models\) is defined for implication goals in the form: \(I\models D\supset G\) iff for all \(I'\) which are extensions of \(I\), \(I'\models D\) implies \(I'\models G\) (\(I,I'\) are Herbrand interpretations). As opposed to a similar approach made by \textit{D. M. Gabbay} and \textit{N. Reyle} [J. Logic Program. 1, 319-355 (1984; Zbl 0576.68001)] no Kripke semantics is really required. However the authors formulate the model theoretic semantics in Kripke style in a later chapter. The authors succeed in introducing the block concept and local declarations (a concept originally developed in imperative languages) in a rigorous logical formalism, which can serve as a firm basis for potential implementations.