Mechanizing structural induction. II: Strategies
From MaRDI portal
Cites work
- A mechanical proof of the termination of Takeuchi's function
- scientific article; zbMATH DE number 3551846 (Why is no real title available?)
- scientific article; zbMATH DE number 3358455 (Why is no real title available?)
- scientific article; zbMATH DE number 3410594 (Why is no real title available?)
- Mechanizing structural induction. I: Formal system
- Mechanizing structural induction. II: Strategies
- Proving Properties of Programs by Structural Induction
- Proving Theorems about LISP Functions
- Recursive data structures
Cited in
(22)- Mechanizing structural induction. I: Formal system
- Mechanizing structural induction. II: Strategies
- PASCAL in LCF: Semantics and examples of proof
- Towards the automation of set theory and its logic
- A strong restriction of the inductive completion procedure
- Sound generalizations in mathematical induction
- Middle-out reasoning for synthesis and induction
- Specification and proof in membership equational logic
- Equivalence checking of two functional programs using inductive theorem provers
- Lean induction principles for tableaux
- Termination of algorithms over non-freely generated data types
- A divergence critic
- Lazy generation of induction hypotheses
- A general framework to build contextual cover set induction provers
- Guiding induction proofs
- Using induction and rewriting to verify and complete parameterized specifications
- Unfolding--definition--folding, in this order, for avoiding unnecessary variables in logic programs
- A unified view of induction reasoning for first-order logic
- Automating induction by reflection
- Proofs by induction in equational theories with constructors
- Mathematical induction in Otter-lambda
- Deaccumulation techniques for improving provability
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)
