A new combination of input and unit deductions for Horn sentences
type: Item
instance of: scholarly article
title: A new combination of input and unit deductions for Horn sentences
zbMATH Open document ID: 0563.68072
DOI: 10.1016/0020-0190(84)90113-3
author: Susumu Yamasaki
author: Mikio Yoshida
author: Shuji Doshita
author: Mikito Hirata
published in: Information Processing Letters
publication date: 1984-01-01T00:00:00Z
review text: A computation of a logic program consists of an input refutation of a set of Horn clauses. To avoid redundant input refutations, the authors propose a combination of input- and unit deduction. It is well known, that a set of clauses is input refutable iff it is unit refutable [\textit{C. L. Chang} and \textit{R. C. T. Lee}: Symbolic logic and mechanical theorem proving (1973; Zbl 0263.68046)]. A possible combination of input- and unit deduction is shown in the following theorem: Let S be a set of Horn clauses and \(C_ 0\) be a negative clause. If there is an input refutation of \(C_ 0\) from S, then there exists a refutation \(C_ 0,D_ 1,...,C_{n-1},D_ n,\square\) where \(D_ 1\) is a unit clause deduced by unit deduction, all \(C_ i\) are resolvents from \(C_{i-1}\) and \(D_ i\) (for \(i\geq 1)\) and all \(D_ i\) for \(i\geq 2\) are in S. A next theorem shows the converse direction. Finally, the authors introduce the concept of ICU deduction; for this kind of deduction, it is prescribed to use also unit-derived unit clauses as side clauses (not only input clauses). The theorems mentioned above guarantee, that ICU refutation realizes the computation of logic programs.
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 68N01
Mathematics Subject Classification ID: 03B35
zbMATH DE Number: 3898268
zbMATH Keywords: logic programming
zbMATH Keywords: resolution
zbMATH Keywords: input refutation
zbMATH Keywords: Horn clauses
reviewed by: Alexander Leitsch
MaRDI profile type: Publication
full work available at URL: 0020-0190(84)90113-3
OpenAlex ID: W2010308603
cites work: The Specialization of Programs by Theorem Proving
cites work: Q4051550
cites work: Q3862380
cites work: Q5672218
cites work: Q5663381
cites work: Q5679703
cites work: Horn clause computability
cites work: The Semantics of Predicate Logic as a Programming Language
Recommended article: Q4357064
Recommended article: Intelligent Backtracking in Plan-Based Deduction
Recommended article: A formal grammatical model of the resolution method for the propositional calculus
Recommended article: Q4366603
Recommended article: Graph-based proof procedures for horn clauses
Recommended article: Unification as a complexity measure for logic programming
Recommended article: Q3133180
Recommended article: Linear and unit-resulting refutations for Horn theories
Recommended article: HORNLOG: A graph-based interpreter for general Horn clauses
Recommended article: Q4539049
description: scientific article; zbMATH DE number 3898268