A strong restriction of the inductive completion procedure
type: Item
instance of: scholarly article
title: A strong restriction of the inductive completion procedure
zbMATH Open document ID: 0682.68029
DOI: 10.1016/S0747-7171(89)80069-0
author: Laurent Fribourg
published in: Journal of Symbolic Computation
publication date: 1989-01-01T00:00:00Z
Mathematics Subject Classification ID: 68W30
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 4117833
zbMATH Keywords: principle of definition
zbMATH Keywords: Knuth-Bendix procedure
zbMATH Keywords: selection function
zbMATH Keywords: ground-confluence
zbMATH Keywords: completion procedure
MaRDI profile type: Publication
cites work: Mechanizing structural induction. II: Strategies
cites work: Q3894958
cites work: Proving Properties of Programs by Structural Induction
cites work: Q3703288
cites work: Q3336735
cites work: Oriented equational clauses as a programming language
cites work: Q3780428
cites work: Q3880309
cites work: Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
cites work: A complete proof of correctness of the Knuth-Bendix completion algorithm
cites work: Q3883561
cites work: Conditional rewrite rules
cites work: Q3709891
cites work: Q3783519
cites work: Q5581665
cites work: Deductive synthesis of the unification algorithm
cites work: Inductive completion with retracts
cites work: Semantic confluence tests and completion methods
cites work: Automated Theorem-Proving for Theories with Simplifiers Commutativity, and Associativity
cites work: Q3783518
cites work: Reasoning about programs
description: scientific article; zbMATH DE number 4117833