ACKERMANN’S FUNCTION IN ITERATIVE FORM: A PROOF ASSISTANT EXPERIMENT

DOI10.1017/BSL.2021.47MaRDI QIDQ5037519zbMATH OpenOpenAlexFDO

Authors Lawrence C. Paulson

Publication date 1 March 2022

Published in The Bulletin of Symbolic Logic (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/2104.11157

zbMATH Keywords

interactive theorem provingIsabelleterminationAckermann's function

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Formalization of mathematics in connection with theorem provers (68V20) Computability and recursion theory (03D99)

Recommendations

• An inherently iterative computation of Ackermann's function
• A note about iterated arithmetic functions
• scientific article; zbMATH DE number 3912360
• Iteration of the φ Function
• The Ackermann constant theorem: A computer-assisted investigation
• On the iteration of a function related to Euler's \(\varphi \)-function
• scientific article; zbMATH DE number 1195591
• scientific article; zbMATH DE number 3903215
• On Iterates of Euler's φ-Function

Cites work

• scientific article; zbMATH DE number 3991418 (Why is no real title available?)
• scientific article; zbMATH DE number 3700811 (Why is no real title available?)
• scientific article; zbMATH DE number 1531624 (Why is no real title available?)
• scientific article; zbMATH DE number 3073037 (Why is no real title available?)
• A consistent foundation for Isabelle/HOL
• Concrete semantics. With Isabelle/HOL
• Isabelle/HOL. A proof assistant for higher-order logic
• On definitions of constants and types in HOL
• Opinion: The Mechanization of Mathematics
• Partial and nested recursive function definitions in higher-order logic
• Tactics for mechanized reasoning: a commentary on Milner (1984) ‘The use of machines to assist in rigorous proof’
• Term Rewriting and All That

Describes a project that uses

Uses Software

• HOL Light
• Isabelle/HOL

This page was built for publication: ACKERMANN’S FUNCTION IN ITERATIVE FORM: A PROOF ASSISTANT EXPERIMENT

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