SLWV - A theorem prover for logic programming

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review


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.

Original languageEnglish
Title of host publicationExtensions of Logic Programming - 3rd International Workshop, ELP 1992, Proceedings
EditorsEvelina Lamina, Paola Mello
Place of PublicationBerlin, Heidelberg
Number of pages23
ISBN (Electronic)978-3-540-47562-0
ISBN (Print)978-3-540-56454-6
Publication statusPublished - 1993
Event3rd International Workshop on Extensions of Logic Programming, ELP 1992 - Bologna, Italy
Duration: 26 Feb 199228 Feb 1992

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume660 LNAI
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference3rd International Workshop on Extensions of Logic Programming, ELP 1992


Dive into the research topics of 'SLWV - A theorem prover for logic programming'. Together they form a unique fingerprint.

Cite this