Ordinal arithmetic: Algorithms and mechanization

DOI10.1007/s10817-005-9023-9zbMath1108.03020OpenAlexW1972787069MaRDI QIDQ851144

Panagiotis Manolios, Daron Vroon

Publication date: 17 November 2006

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

Full work available at URL: https://doi.org/10.1007/s10817-005-9023-9

zbMATH Keywords

theorem provingautomated reasoningordinal arithmeticterminationACL2compact ordinal notations

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Ordinal and cardinal numbers (03E10)

Related Items

Type-theoretic approaches to ordinals, The Ideal Approach to Computing Closed Subsets in Well-Quasi-orderings, Beyond polynomials and Peano arithmetic -- automation of elementary and ordinal interpretations, Inference rules for proving the equivalence of recursive procedures, Inference Rules for Proving the Equivalence of Recursive Procedures

Uses Software

• ACL2
• Coq
• Isabelle
• ML
• PVS
• Mizar
• Isabelle/ZF
• HOL
• NQTHM

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Set theory. An introduction to independence proofs
• What's so special about Kruskal's theorem and the ordinal \(\Gamma{}_ 0\)? A survey of some results in proof theory
• Computer proofs in Gödel's class theory with equational definitions for composite and cross
• On computer-assisted proofs in ordinal number theory
• Set theory for verification. I: From foundations to functions
• Isabelle. A generic theorem prover
• Partial functions in ACL2
• Set theory for verification. II: Induction and recursion
• Normal functions and constructive ordinal notations
• A Mechanically Checked Proof of IEEE Compliance of the Floating Point Multiplication, Division and Square Root Algorithms of the AMD-K7^™ Processor
• Term Rewriting and All That
• The Relative Consistency of the Axiom of Choice Mechanized Using Isabelle⁄zf
• Formal Methods in Computer-Aided Design
• An extended arithmetic of ordinal numbers
• Systems of Logic Based on Ordinals^†
• Automated Deduction – CADE-19
• Automated Deduction – CADE-19
• The consistency of arithmetics
• Mechanizing set theory. Cardinal arithmetic and the axiom of choice