scientific article; zbMATH DE number 3891336

MaRDI QIDQ3347863zbMATH OpenFDO

Authors

Publication date 1984

zbMATH Keywords

inductive completenesssimplification of equationsterm rewriting system

Mathematics Subject Classification ID

Equational classes, universal algebra in model theory (03C05) Free algebras (08B20)

Recommendations

• Proofs by induction in equational theories with constructors
• Automatic proofs by induction in theories without constructors
• scientific article; zbMATH DE number 3956434
• A strong restriction of the inductive completion procedure
• scientific article; zbMATH DE number 4047063

Cited in

(27)

• Inductive proof search modulo
• Equational methods in first order predicate calculus
• Partial evaluation and \(\omega\)-completeness of algebraic specifications
• On solving the equality problem in theories defined by Horn clauses
• Proof by consistency
• Equivalences and transformations of regular systems - applications to recursive program schemes and grammars
• A criterion for proving noetherianity of a relation
• The equational part of proofs by structural induction
• Which data types have -complete initial algebra specifications?
• Intuitionistic Podelski-Rybalchenko theorem and equivalence between inductive definitions and cyclic proofs
• A strong restriction of the inductive completion procedure
• Automatic proofs by induction in theories without constructors
• Constructor-Based Inductive Theorem Prover
• Sound lemma generation for proving inductive validity of equations
• scientific article; zbMATH DE number 3870639 (Why is no real title available?)
• scientific article; zbMATH DE number 4164162 (Why is no real title available?)
• scientific article; zbMATH DE number 4166886 (Why is no real title available?)
• scientific article; zbMATH DE number 3956434 (Why is no real title available?)
• scientific article; zbMATH DE number 4047063 (Why is no real title available?)
• scientific article; zbMATH DE number 4074451 (Why is no real title available?)
• Inductive proofs by specification transformations
• Proving equational and inductive theorems by completion and embedding techniques
• Computer Science Logic
• Tools for proving inductive equalities, relative completeness, and \(\omega\)-completeness
• Proof by consistency in conditional equational theories
• Automating inductionless induction using test sets
• Proofs by induction in equational theories with constructors

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3347863)