Function definition in higher-order logic

DOI10.1007/BFB0105417MaRDI QIDQ6567726zbMATH OpenFDO

Authors Konrad Slind

Publication date 5 July 2024

Full work available at URL https://doi.org/10.1007/BFB0105417

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Partial Recursive Functions in Higher-Order Logic
• Partial and nested recursive function definitions in higher-order logic
• scientific article; zbMATH DE number 2185679
• Adapting functional programs to higher order logic
• Partiality and recursion in higher-order logic

Cites work

• A higher-order implementation of rewriting
• A typed pattern calculus
• A user's friendly syntax to define recursive functions as typed λ-terms
• Automatizing termination proofs of recursively defined functions
• Constructing recursion operators in intuitionistic type theory
• scientific article; zbMATH DE number 2185679 (Why is no real title available?)
• scientific article; zbMATH DE number 4045703 (Why is no real title available?)
• scientific article; zbMATH DE number 3702108 (Why is no real title available?)
• scientific article; zbMATH DE number 806754 (Why is no real title available?)
• On proving the termination of algorithms by machine
• Proving termination of normalization functions for conditional expressions
• Rippling: A heuristic for guiding inductive proofs
• Term rewriting and beyond -- theorem proving in Isabelle
• Terminating general recursion
• The Alf proof editor and its proof engine

This page was built for publication: Function definition in higher-order logic

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