Ordinal arithmetic: Algorithms and mechanization
From MaRDI portal
Publication:851144
DOI10.1007/s10817-005-9023-9zbMath1108.03020MaRDI 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
theorem proving; automated reasoning; ordinal arithmetic; termination; ACL2; compact ordinal notations
Uses Software
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
