Mechanizing structural induction. I: Formal system

DOI10.1016/0304-3975(79)90034-3zbMath0423.68050OpenAlexW2077789910WikidataQ127939632 ScholiaQ127939632MaRDI QIDQ1134540

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)90034-3

zbMATH Keywords

structural inductionprogram properties

Mathematics Subject Classification ID

Abstract data types; algebraic specification (68Q65)

Related Items

Verifying Procedural Programs via Constrained Rewriting Induction ⋮ Foundations of a theorem prover for functional and mathematical uses ⋮ Mathematical induction in Otter-lambda ⋮ Reasoning with conditional axioms ⋮ Mechanizing structural induction. II: Strategies

Uses Software

• NQTHM

Cites Work

• 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
• Unnamed Item
• Unnamed Item

This page was built for publication: Mechanizing structural induction. I: Formal system