Ordinal arithmetic: Algorithms and mechanization
From MaRDI portal
Recommendations
Cites work
- scientific article; zbMATH DE number 1678386 (Why is no real title available?)
- scientific article; zbMATH DE number 50008 (Why is no real title available?)
- scientific article; zbMATH DE number 473381 (Why is no real title available?)
- scientific article; zbMATH DE number 1497485 (Why is no real title available?)
- scientific article; zbMATH DE number 1863385 (Why is no real title available?)
- scientific article; zbMATH DE number 2090314 (Why is no real title available?)
- scientific article; zbMATH DE number 2102719 (Why is no real title available?)
- scientific article; zbMATH DE number 1390279 (Why is no real title available?)
- scientific article; zbMATH DE number 1420856 (Why is no real title available?)
- scientific article; zbMATH DE number 234014 (Why is no real title available?)
- scientific article; zbMATH DE number 3392437 (Why is no real title available?)
- scientific article; zbMATH DE number 3024905 (Why is no real title available?)
- scientific article; zbMATH DE number 3071176 (Why is no real title available?)
- A Mechanically Checked Proof of IEEE Compliance of the Floating Point Multiplication, Division and Square Root Algorithms of the AMD-K7™ Processor
- Algorithms for ordinal arithmetic.
- An extended arithmetic of ordinal numbers
- Computer proofs in Gödel's class theory with equational definitions for composite and cross
- Formal Methods in Computer-Aided Design
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Isabelle. A generic theorem prover
- Mechanizing set theory. Cardinal arithmetic and the axiom of choice
- Normal functions and constructive ordinal notations
- On computer-assisted proofs in ordinal number theory
- Partial functions in ACL2
- Reasoning about iteration in Gödel's class theory.
- Set theory for verification. I: From foundations to functions
- Set theory for verification. II: Induction and recursion
- Set theory. An introduction to independence proofs
- Systems of Logic Based on Ordinals†
- Term Rewriting and All That
- The Relative Consistency of the Axiom of Choice Mechanized Using Isabelle⁄zf
- The consistency of arithmetics
- What's so special about Kruskal's theorem and the ordinal \(\Gamma{}_ 0\)? A survey of some results in proof theory
Cited in
(13)- Formal Methods in Computer-Aided Design
- The ideal approach to computing closed subsets in well-quasi-orderings
- Inference rules for proving the equivalence of recursive procedures
- A mechanizable first-order theory of ordinals
- Algorithms for ordinal arithmetic.
- Ordinal arithmetic based on Skolem hulling
- Type-theoretic approaches to ordinals
- Ordinals in HOL: transfinite arithmetic up to (and beyond) \(\omega _{1}\)
- Natural addition of ordinals
- Inference rules for proving the equivalence of recursive procedures
- An ordinal calculus for proving termination in term rewriting
- Beyond polynomials and Peano arithmetic -- automation of elementary and ordinal interpretations
- Trees, ordinals and termination
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)
