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

DOI10.1017/bsl.2021.47OpenAlexW3204935188MaRDI QIDQ5037519

Lawrence Charles 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

zbMATH Keywords

terminationinteractive theorem provingIsabelleAckermann's function

Mathematics Subject Classification ID

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

Uses Software

• Isabelle/HOL
• HOL Light

Cites Work

• On definitions of constants and types in HOL
• Partial and nested recursive function definitions in higher-order logic
• Isabelle/HOL. A proof assistant for higher-order logic
• A consistent foundation for Isabelle/HOL
• Concrete Semantics
• Tactics for mechanized reasoning: a commentary on Milner (1984) ‘The use of machines to assist in rigorous proof’
• Opinion: The Mechanization of Mathematics
• Term Rewriting and All That
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

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