Mechanizing structural induction. II: Strategies
From MaRDI portal
Cites work
- 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?)
- A mechanical proof of the termination of Takeuchi's function
- 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
(20)- PASCAL in LCF: Semantics and examples of proof
- Equivalence checking of two functional programs using inductive theorem provers
- Deaccumulation techniques for improving provability
- Mechanizing structural induction. II: Strategies
- Lean induction principles for tableaux
- A divergence critic
- 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
- Mechanizing structural induction. I: Formal system
- Termination of algorithms over non-freely generated data types
- 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
- Unfolding--definition--folding, in this order, for avoiding unnecessary variables in logic programs
- Middle-out reasoning for synthesis and induction
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)
