Sound lemma generation for proving inductive validity of equations

DOI10.4230/LIPICS.FSTTCS.2008.1737MaRDI QIDQ3165943zbMATH OpenOpenAlexFDO

Authors Takahito Aoto

Publication date 19 October 2012

Full work available at URL http://subs.emis.de/LIPIcs/frontdoor_164a.html

zbMATH Keywords

automated theorem provinginductive theoremsound generalizationterm rewriting

Mathematics Subject Classification ID

Recommendations

• Sound generalizations in mathematical induction
• An algebraic characterization of inductive soundness in proof by consistency
• Proofs by induction in equational theories with constructors
• scientific article; zbMATH DE number 3891336
• The equational part of proofs by structural induction
• Proving equational and inductive theorems by completion and embedding techniques
• Lemma discovery in automating induction
• scientific article; zbMATH DE number 4074541
• On the generation of quantified lemmas
• Soundness and completeness proofs by coinductive methods

Cited in

(5)

• Appropriate lemmae discovery
• Sound generalizations in mathematical induction
• On the generation of quantified lemmas
• Improvements in Formula Generalization
• Correctness of Context-Moving Transformations for Term Rewriting Systems

Describes a project that uses

Uses Software

• ACL2
• InKa
• RRL

This page was built for publication: Sound lemma generation for proving inductive validity of equations

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