Mechanizing structural induction. II: Strategies

DOI10.1016/0304-3975(79)90035-5zbMath0423.68051OpenAlexW2009923373WikidataQ128039954 ScholiaQ128039954MaRDI QIDQ1134541

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

zbMATH Keywords

structural inductionsearch strategiesprogram properties

Mathematics Subject Classification ID

Related Items (19)

Sound generalizations in mathematical induction ⋮ Mathematical induction in Otter-lambda ⋮ Middle-out reasoning for synthesis and induction ⋮ Equivalence checking of two functional programs using inductive theorem provers ⋮ Deaccumulation techniques for improving provability ⋮ Mechanizing structural induction. I: Formal system ⋮ Mechanizing structural induction. II: Strategies ⋮ Lean induction principles for tableaux ⋮ Specification and proof in membership equational logic ⋮ Using induction and rewriting to verify and complete parameterized specifications ⋮ Unfolding--definition--folding, in this order, for avoiding unnecessary variables in logic programs ⋮ Termination of algorithms over non-freely generated data types ⋮ A general framework to build contextual cover set induction provers ⋮ PASCAL in LCF: Semantics and examples of proof ⋮ Towards the automation of set theory and its logic ⋮ A divergence critic ⋮ Lazy generation of induction hypotheses ⋮ A strong restriction of the inductive completion procedure ⋮ Proofs by induction in equational theories with constructors

Uses Software

• NQTHM

Cites Work

• Mechanizing structural induction. I: Formal system
• Mechanizing structural induction. II: Strategies
• A mechanical proof of the termination of Takeuchi's function
• Recursive data structures
• Proving Theorems about LISP Functions
• Proving Properties of Programs by Structural Induction
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Mechanizing structural induction. II: Strategies