SLWV - A theorem prover for logic programming

The purpose of this work is to define a theorem prover that retains the procedural aspects of logic programing. The proof system we propose (SLWV-resolution, for Selected Linear Without contrapositive clause Variants)) is defined for a set of clauses in the hnplicational form (keeping to the form of logic programs), not requiring contrapositives, and has an execution method that respects the execution order of literals in a clause, preserving the procedural flavor of logic programming. SLWV-resolution can be seen as a combination of SL-resolution and case-analysis, which admits a form of linear derivation. We show its soundness and completeness by establishing a one-toone mapping between SLWV and SL derivations which also clarifies the motivation and the method.Our work can be seen as an extension to logic programs that goes beyond normal programs, and thus beyond (positive) definite clause programming, by allowing also definite negative heads. Thus we admit program clauses with both positive and (classically) negated atoms conjoined in the body, and at. most one literal as its head (clauses with disjunctions of literals in the head are transformed into a single clause of that form). As this approach doe.s not require clause contrapositives and admits a leftmost selection function, the implementation can and does preserve the pragmatic procedural reading explicitly provided by the programmer. The implementation, not described here. relies on the source program being preprocessed into directly executable Prolog. Preprocessing keeps the overall program structure untouched, and thus a directly recognizable execution pattern that mimics Prolog is obtained: this is useful in debugging. Additionally, the preprocessing is such that Prolog programs run with negligible overhead. Various program examples and attending derivations are proffered.