Non-Horn clause logic programming without contrapositives
type: Item
instance of: scholarly article
title: Non-Horn clause logic programming without contrapositives
zbMATH Open document ID: 0666.68091
DOI: 10.1007/BF00244944
published in: Journal of Automated Reasoning
publication date: 1988-01-01T00:00:00Z
review text: 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.
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 4090845
zbMATH Keywords: logic programming
zbMATH Keywords: caching
zbMATH Keywords: Horn-Clauses
zbMATH Keywords: proof search
zbMATH Keywords: splitting rule
zbMATH Keywords: theorem prover
zbMATH Keywords: rewriting
author: David A. Plaisted
reviewed by: G. E. Mints
MaRDI profile type: Publication
full work available at URL: https://doi.org/10.1007/bf00244944
OpenAlex ID: W1998330152
Recommended article: Non-Horn clause logic programming
Recommended article: Q3820058
Recommended article: Q4840654
Recommended article: Q3827538
Recommended article: Q3365575
Recommended article: Q4282552
Recommended article: Programming in logic without logic programming
Recommended article: Q3769956
Recommended article: Semantics for logic programs without occur check
description: scientific article; zbMATH DE number 4090845