Near-Horn PROLOG

The Near-Horn Prolog procedures have been proposed as e ective procedures in the area of disjunctive logic programming, an extension of logic programming to the ( rstorder) non-Horn clause domain. In this paper, we show that these case-analysis based procedures may be viewed as members of a class of procedures called the \ancestry family," which also includes Model Elimination (and its variants), the Positive Re nement of Model Elimination, and SLWV-resolution. The common feature which binds these procedures is the extension of SLD-resolution to full rst-order logic with the addition of an ancestor cancellation rule. Procedures in the ancestry family are all sound and complete rst-order procedures that can be seen to vary along three parameters: (1) the number of clause contrapositives required, (2) the amount of ancestor checking that must occur, and (3) the use (if any) of a Restart rule. Using a sequent-style presentation format for all procedures, we highlight the close relat...

• Type: Conference
• Year: 1987
• Where: ICLP
• Authors: Donald W. Loveland
• Keywords: Automated Reasoning, Case-analysis Based Procedures, ICLP 1987, Near-Horn Prolog Procedures, Procedures