Non-Horn clause logic programming without contrapositives (Q1116717)

The simplified reduction format proposed by the author deals with initial clauses \(L_ 1,...,L_ k\to M_ 1\vee...\vee M_ n\) and derives Horn- Clauses. (Everything is presented for the propositional case but lifts to the predicate case). To each initial clause corresponds the rule (up to unification) \[ X\to L_ 1;\quad...;\quad X\to L_ k;\quad X, M_ 1\to V;\quad...,;\quad X, M_ k\to U \vdash X\to U. \] Variation of it deals with clauses of the form \(L_ 1\vee...\vee L_ k\vee \neg M_ 1\vee...\vee \neg M_{n-1}\to M,\) has the basic rule of the form \[ X\to L_ 1;\quad...;\quad X\to L_ k;\quad X\to \neg M_ 1;\quad...;\quad X\to \neg M_ k \vdash X\to M \] and the splitting rule \(X, \neg L\to M;\quad X, l\to M \vdash X\to M.\) The modified reduction format is intended to optimize proof search in the latter version by controlling negative subgoals and the splitting rules. Its derivable objects are sequents \(X\to L\Rightarrow Y\to L\) where X is contained in Y. Axioms are \(X\to L\Rightarrow X\to L\) for \(L\in X\), and \(X\to \vdash L\Rightarrow X, \neg L\to \neg L\) for all relevant atoms L. The domain rule for the initial clause \(L_ 1,...,L_ n\to L\) (with arbitrary literals) is \[ X_ 0\to L_ 1\Rightarrow X_ 1\to L_ 1;\quad X_ 1\to L_ 2\Rightarrow X_ 2\to L_ 2;\quad...;\quad X_{n-1}\to L_ n\Rightarrow X_ n\to L_ n \vdash X_ 0\to L\Rightarrow X_ n\to L\quad. \] The splitting rule has the following form with \(| X| \leq | Y|:\) \[ X\to L\Rightarrow Y, \neg M\to L;\quad Y, M\to L\Rightarrow Y, M\Rightarrow L \vdash X\to L\Rightarrow Y\to L\quad. \] Unsatisfiability of a set of clauses is equivalent to derivability of FALSE\(\Rightarrow FALSE\). The theorem prover based on the simplification of these rules is described. The range of provable predicate formulas seems to be approximately the same as for Stickel's program [\textit{M. E. Stickel}, Lect. Notes Comput. Sci. 230, 573-587 (1986; Zbl 0609.68065)]. There are also rewriting facilities for dealing with equality.