ACKERMANN’S FUNCTION IN ITERATIVE FORM: A PROOF ASSISTANT EXPERIMENT
From MaRDI portal
Publication:5037519
DOI10.1017/BSL.2021.47OpenAlexW3204935188MaRDI QIDQ5037519FDOQ5037519
Authors: Lawrence C. Paulson 
Publication date: 1 March 2022
Published in: The Bulletin of Symbolic Logic (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/2104.11157
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
Mechanization of proofs and logical operations (03B35) Formalization of mathematics in connection with theorem provers (68V20) Computability and recursion theory (03D99)
Cites Work
- Title not available (Why is that?)
- Isabelle/HOL. A proof assistant for higher-order logic
- Title not available (Why is that?)
- Term Rewriting and All That
- On definitions of constants and types in HOL
- Concrete semantics. With Isabelle/HOL
- Partial and nested recursive function definitions in higher-order logic
- Title not available (Why is that?)
- Title not available (Why is that?)
- A consistent foundation for Isabelle/HOL
- Opinion: The Mechanization of Mathematics
- Tactics for mechanized reasoning: a commentary on Milner (1984) ‘The use of machines to assist in rigorous proof’
Uses Software
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)
