Proofs by induction in equational theories with constructors
type: Item
instance of: scholarly article
title: Proofs by induction in equational theories with constructors
zbMATH Open document ID: 0532.68041
DOI: 10.1016/0022-0000(82)90006-X
author: Gérard Huet
author: Jean-Marie Hullot
published in: Journal of Computer and System Sciences
publication date: 1982-01-01T00:00:00Z
Mathematics Subject Classification ID: 68Q65
Mathematics Subject Classification ID: 08B05
Mathematics Subject Classification ID: 68N01
Mathematics Subject Classification ID: 08-04
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 3845044
zbMATH Keywords: program proving
zbMATH Keywords: equational logic
zbMATH Keywords: initial algebra of an equational variety
zbMATH Keywords: extension of the Knuth-Bendix completion algorithm
zbMATH Keywords: data structures
zbMATH Keywords: algebraic-summation identities
MaRDI profile type: Publication
cites work: Mechanizing structural induction. II: Strategies
cites work: Proving Theorems about LISP Functions
cites work: Q3894958
cites work: Proving Properties of Programs by Structural Induction
cites work: Q3880309
cites work: Initial Algebra Semantics and Continuous Algebras
cites work: Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
cites work: Q5581665
cites work: New decision algorithms for finitely presented commutative semigroups
full work available at URL: 0022-0000(82)90006-x
OpenAlex ID: W2021173362
description: scientific article; zbMATH DE number 3845044