Mechanizing structural induction. I: Formal system

DOI10.1016/0304-3975(79)90034-3MaRDI QIDQ1134540zbMATH OpenOpenAlexWikidataFDO

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

zbMATH Keywords

structural inductionprogram properties

Mathematics Subject Classification ID

Abstract data types; algebraic specification (68Q65)

Cites work

• scientific article; zbMATH DE number 3551846 (Why is no real title available?)
• scientific article; zbMATH DE number 3436590 (Why is no real title available?)
• scientific article; zbMATH DE number 3227055 (Why is no real title available?)
• scientific article; zbMATH DE number 3247155 (Why is no real title available?)
• scientific article; zbMATH DE number 3296221 (Why is no real title available?)
• A mechanical proof of the termination of Takeuchi's function
• Mechanizing structural induction. II: Strategies
• Proving Properties of Programs by Structural Induction
• Proving Theorems about LISP Functions
• Recursive data structures

Cited in

(5)

• Mechanizing structural induction. II: Strategies
• Mathematical induction in Otter-lambda
• Verifying procedural programs via constrained rewriting induction
• Foundations of a theorem prover for functional and mathematical uses
• Reasoning with conditional axioms

Describes a project that uses

Uses Software

• NQTHM

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1134540)