A new combination of input and unit deductions for Horn sentences (Q1057665)

A computation of a logic program consists of an input refutation of a set of Horn clauses. To avoid redundant input refutations, the authors propose a combination of input- and unit deduction. It is well known, that a set of clauses is input refutable iff it is unit refutable [\textit{C. L. Chang} and \textit{R. C. T. Lee}: Symbolic logic and mechanical theorem proving (1973; Zbl 0263.68046)]. A possible combination of input- and unit deduction is shown in the following theorem: Let S be a set of Horn clauses and \(C_ 0\) be a negative clause. If there is an input refutation of \(C_ 0\) from S, then there exists a refutation \(C_ 0,D_ 1,...,C_{n-1},D_ n,\square\) where \(D_ 1\) is a unit clause deduced by unit deduction, all \(C_ i\) are resolvents from \(C_{i-1}\) and \(D_ i\) (for \(i\geq 1)\) and all \(D_ i\) for \(i\geq 2\) are in S. A next theorem shows the converse direction. Finally, the authors introduce the concept of ICU deduction; for this kind of deduction, it is prescribed to use also unit-derived unit clauses as side clauses (not only input clauses). The theorems mentioned above guarantee, that ICU refutation realizes the computation of logic programs.