Ordinal arithmetic: Algorithms and mechanization

DOI10.1007/S10817-005-9023-9zbMATH Open1108.03020OpenAlexW1972787069MaRDI QIDQ851144FDOQ851144

Authors: 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

Recommendations

• Algorithms for ordinal arithmetic.
• Formal Methods in Computer-Aided Design
• Ordinals in HOL: transfinite arithmetic up to (and beyond) \(\omega _{1}\)
• A mechanizable first-order theory of ordinals
• An ordinal calculus for proving termination in term rewriting

zbMATH Keywords

theorem provingautomated reasoningterminationACL2ordinal arithmeticcompact ordinal notations

Mathematics Subject Classification ID

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

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Set theory. An introduction to independence proofs
• Isabelle. A generic theorem prover
• The consistency of arithmetics
• Term Rewriting and All That
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Set theory for verification. I: From foundations to functions
• Partial functions in ACL2
• The Relative Consistency of the Axiom of Choice Mechanized Using Isabelle⁄zf
• Systems of Logic Based on Ordinals^†
• A Mechanically Checked Proof of IEEE Compliance of the Floating Point Multiplication, Division and Square Root Algorithms of the AMD-K7^™ Processor
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• On computer-assisted proofs in ordinal number theory
• An extended arithmetic of ordinal numbers
• 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
• Set theory for verification. II: Induction and recursion
• Title not available (Why is that?)
• Normal functions and constructive ordinal notations
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Formal Methods in Computer-Aided Design
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Reasoning about iteration in Gödel's class theory.
• Algorithms for ordinal arithmetic.
• Mechanizing set theory. Cardinal arithmetic and the axiom of choice

Cited In (13)

• Type-theoretic approaches to ordinals
• Formal Methods in Computer-Aided Design
• Natural addition of ordinals
• An ordinal calculus for proving termination in term rewriting
• Algorithms for ordinal arithmetic.
• Trees, ordinals and termination
• Beyond polynomials and Peano arithmetic -- automation of elementary and ordinal interpretations
• Ordinal arithmetic based on Skolem hulling
• A mechanizable first-order theory of ordinals
• Inference rules for proving the equivalence of recursive procedures
• The ideal approach to computing closed subsets in well-quasi-orderings
• Ordinals in HOL: transfinite arithmetic up to (and beyond) \(\omega _{1}\)
• Inference rules for proving the equivalence of recursive procedures

Uses Software

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

This page was built for publication: Ordinal arithmetic: Algorithms and mechanization

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