Parsing as non-Horn deduction (Q688151)

In the the author's paper [Artif. Intell. 63, 225-264 (1963)] the logic programming techniques for collecting answers from Horn clause resolution proofs to the non-Horn case were extended. By a defined program we shall mean a finite set of clauses of the form \(A \leftarrow B_ 1, \dots, B_ n\). Reiter introduced the well known rule CWA, called closed world assumption: if an atom \(A\) without variables is not a consequence of a defined program, then we conclude \(\neg A\). So we can get a negative result by a refutation of a positive result. The second non-monotone rule was studied by Clark: if an atom \(A\) is in SLD-set of finite refutation of a defined program \(P\), then we conclude \(\neg A\). This rule is weaker than CWA rule. In the considered paper some generalization of Clark's theorem is proved: if \(\Gamma\) is a refutation of \(T \cup S\) where \(A\) is the answer set for \(S\) in \(\Gamma\), then \(T \models \forall \neg A\). Non- Horn reasoning is required to establish negative results, i.e. to refute positive results. It was introduced the answer set for \(S\) in deduction \(\Gamma\), as the special set of clauses. The main result is the strong completeness for sets of clauses \(S\): if \(T \models \neg SQ\), then there is a refutation \(\Gamma\) of \(T \cup S\) with answer set \(A\) such that every clause in \(SQ\) is an instance of a clause in \(A\).