Mechanizing structural induction. II: Strategies
From MaRDI portal
Publication:1134541
DOI10.1016/0304-3975(79)90035-5zbMATH Open0423.68051OpenAlexW2009923373WikidataQ128039954 ScholiaQ128039954MaRDI QIDQ1134541FDOQ1134541
Authors: Raymond Aubin 
Publication date: 1979
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/0304-3975(79)90035-5
Cites Work
- Title not available (Why is that?)
- Proving Theorems about LISP Functions
- Proving Properties of Programs by Structural Induction
- Title not available (Why is that?)
- A mechanical proof of the termination of Takeuchi's function
- Mechanizing structural induction. II: Strategies
- Mechanizing structural induction. I: Formal system
- Recursive data structures
- Title not available (Why is that?)
Cited In (20)
- PASCAL in LCF: Semantics and examples of proof
- Equivalence checking of two functional programs using inductive theorem provers
- Lean induction principles for tableaux
- Deaccumulation techniques for improving provability
- A divergence critic
- Mechanizing structural induction. II: Strategies
- Guiding induction proofs
- Sound generalizations in mathematical induction
- Using induction and rewriting to verify and complete parameterized specifications
- Proofs by induction in equational theories with constructors
- Mathematical induction in Otter-lambda
- Termination of algorithms over non-freely generated data types
- Mechanizing structural induction. I: Formal system
- Towards the automation of set theory and its logic
- Specification and proof in membership equational logic
- Lazy generation of induction hypotheses
- A strong restriction of the inductive completion procedure
- A general framework to build contextual cover set induction provers
- Middle-out reasoning for synthesis and induction
- Unfolding--definition--folding, in this order, for avoiding unnecessary variables in logic programs
Uses Software
This page was built for publication: Mechanizing structural induction. II: Strategies
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1134541)
