Induction proofs with partial functions

DOI10.1023/A:1006408829523MaRDI QIDQ1595923zbMATH OpenFDO

Authors Jürgen Giesl

Publication date 18 February 2001

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1023/A:1006408829523

zbMATH Keywords

automated theorem provinginductionpartial functions

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Review text

The author presents a method for automated induction proofs about partial functions. The method is obtained by restricting the rules usually applied in automated theorem proving. A new calculus for induction proofs with partial functions is developed. Several applications requiring reasoning about partial functions are discussed.

Recommendations

• scientific article; zbMATH DE number 3880144
• scientific article; zbMATH DE number 4074542
• scientific article; zbMATH DE number 4102511
• The automation of proof by mathematical induction
• Partial Recursive Functions in Higher-Order Logic

Cited in

(14)

• Rule-based induction
• scientific article; zbMATH DE number 1696825 (Why is no real title available?)
• scientific article; zbMATH DE number 3880144 (Why is no real title available?)
• A two-valued logic for properties of strict functional programs allowing partial functions
• scientific article; zbMATH DE number 3986670 (Why is no real title available?)
• scientific article; zbMATH DE number 4062640 (Why is no real title available?)
• scientific article; zbMATH DE number 4074542 (Why is no real title available?)
• Automatic verification of functions with accumulating parameters
• scientific article; zbMATH DE number 2043540 (Why is no real title available?)
• scientific article; zbMATH DE number 1405455 (Why is no real title available?)
• Partiality and recursion in interactive theorem provers -- an overview
• Correctness of Context-Moving Transformations for Term Rewriting Systems
• Reasoning about incompletely defined programs
• Partial and nested recursive function definitions in higher-order logic

This page was built for publication: Induction proofs with partial functions

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