Automatic derivation and application of induction schemes for mutually recursive functions

DOI10.1007/3-540-44957-4_42MaRDI QIDQ2767092zbMATH OpenFDO

Authors Konrad Slind, Richard Boulton

Publication date 28 January 2002

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-44957-4_42

Mathematics Subject Classification ID

Recommendations

• Induction proofs with partial functions
• Derivation and use of induction schemes in higher-order logic
• Induction using term orderings
• scientific article; zbMATH DE number 3880144
• Induction using term orders

Cited in

(5)

• AN EXTENSION OF AN AUTOMATED TERMINATION METHOD OF RECURSIVE FUNCTIONS
• Mechanically certifying formula-based Noetherian induction reasoning
• Advances in Computing Science – ASIAN 2003. Progamming Languages and Distributed Computation Programming Languages and Distributed Computation
• Generating mutually inductive theorems from concise descriptions
• A unified view of induction reasoning for first-order logic

Describes a project that uses

Uses Software

• CLAM
• HOL

This page was built for publication: Automatic derivation and application of induction schemes for mutually recursive functions

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