Automatic proofs by induction in theories without constructors
type: Item
instance of: scholarly article
title: Automatic proofs by induction in theories without constructors
zbMATH Open document ID: 0682.68032
DOI: 10.1016/0890-5401(89)90062-X
author: Jean-Pierre Jouannaud
author: Emmanuel Kounalis
published in: Information and Computation
publication date: 1989-01-01T00:00:00Z
Mathematics Subject Classification ID: 68W30
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 03D03
Mathematics Subject Classification ID: 68Q65
zbMATH DE Number: 4117836
zbMATH Keywords: Inductionless induction
zbMATH Keywords: equational reasoning
zbMATH Keywords: initial algebra
zbMATH Keywords: Knuth- Bendix completion algorithm
zbMATH Keywords: inductive completion algorithm
zbMATH Keywords: inductive reducibility
zbMATH Keywords: inductive co-reducibility
zbMATH Keywords: term rewriting systems
MaRDI profile type: Publication
cites work: Process algebra for synchronous communication
cites work: Q3894958
cites work: Q3785921
cites work: Q3703288
cites work: Q3725540
cites work: Q3880309
cites work: Q3719824
cites work: Q3687683
cites work: Q3028369
cites work: A complete proof of correctness of the Knuth-Bendix completion algorithm
cites work: Proofs by induction in equational theories with constructors
cites work: Completion of a Set of Rules Modulo a Set of Equations
cites work: REVEUR-3: The implementation of a general completion procedure parameterized by built-in theories and strategies
cites work: Q5581665
cites work: Q3713575
cites work: An overview of the Tecton proof system
cites work: Q3347863
cites work: Q3698310
cites work: Q3716284
cites work: Q3696496
cites work: Q3783518
full work available at URL: 0890-5401(89)90062-x
OpenAlex ID: W2056774266
description: scientific article; zbMATH DE number 4117836