Refutational theorem proving using term-rewriting systems
type: Item
instance of: scholarly article
title: Refutational theorem proving using term-rewriting systems
zbMATH Open document ID: 0558.68072
DOI: 10.1016/0004-3702(85)90074-8
author: Jieh Hsiang
published in: Artificial Intelligence
publication date: 1985-01-01T00:00:00Z
full work available at URL: 20.pdf
review text: The paper proposes a new approach to theorem proving in first-order logic based on term-rewriting systems. First, for propositional calculus a canonical term-rewriting system for Boolean algebra is introduced. The key point enabling successful construction of the canonical term- rewriting system (in contrast with all the previous attempts that failed due to the fact that the prime implicant representation of Boolean terms is not unique) consists in choosing exclusive or instead of or. The canonical system for Boolean algebra enables transformation of the first- order calculus into a form of equational logic and to develop several complete strategies (both clausal and nonclausal) for first-order theories based on the Knuth-Bendix completion algorithm. These strategies deal with predicate logic and built-in (equational) theories in a uniform and quite efficient way. Comparison of implementation of a theorem prover based on term-rewriting with other theorem provers based on locking reduction or natural deduction shows that the method proposed is in general much more efficient then the methods based on resolution. Great efficiency and easy modifiability of a theorem prover based on the term-rewriting method makes the method a serious counterpart to resolution and it will probably have significant impact on theorem proving.
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 03B30
Mathematics Subject Classification ID: 03B35
Mathematics Subject Classification ID: 03B10
Mathematics Subject Classification ID: 06E20
Mathematics Subject Classification ID: 08A50
zbMATH DE Number: 3890764
zbMATH Keywords: first-order logic
zbMATH Keywords: Boolean algebra
zbMATH Keywords: equational logic
Wikidata QID: Q56039144
reviewed by: Jiří Zlatuška
describes a project that uses: REVE
MaRDI profile type: Publication
OpenAlex ID: W2019751493
cites work: Non-resolution theorem proving
cites work: Proving Theorems with the Modification Method
cites work: Q5679729
cites work: Q4138187
cites work: Orderings for term-rewriting systems
cites work: Q3338216
cites work: A complete proof of correctness of the Knuth-Bendix completion algorithm
cites work: Q3883561
cites work: Q3659124
cites work: Completion of a Set of Rules Modulo a Set of Equations
cites work: Q3338225
cites work: Q5581665
cites work: Q5621960
cites work: New decision algorithms for finitely presented commutative semigroups
cites work: Q4124327
cites work: Complete Sets of Reductions for Some Equational Theories
cites work: A simplified problem reduction format
cites work: Q5678447
cites work: Theorem-Proving on the Computer
cites work: A Machine-Oriented Logic Based on the Resolution Principle
cites work: Q5591533
cites work: Q3707399
cites work: Experiment with an automatic theorem-prover having partial ordering inference rules
cites work: Automated Theorem-Proving for Theories with Simplifiers Commutativity, and Associativity
cites work: A Unification Algorithm for Associative-Commutative Functions
cites work: Computer-Implemented Set Theory
cites work: Q3745825
description: scientific article; zbMATH DE number 3890764