Ordinal arithmetic: Algorithms and mechanization (Q851144): Difference between revisions

@@ Property / describes a project that uses @@
+HOL
@@ Property / describes a project that uses: HOL / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+NQTHM
@@ Property / describes a project that uses: NQTHM / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Isabelle
@@ Property / describes a project that uses: Isabelle / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+PVS
@@ Property / describes a project that uses: PVS / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Coq
@@ Property / describes a project that uses: Coq / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+ML
@@ Property / describes a project that uses: ML / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Isabelle/ZF
@@ Property / describes a project that uses: Isabelle/ZF / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1007/s10817-005-9023-9
+Normal rank
@@ Property / OpenAlex ID @@
+W1972787069
@@ Property / OpenAlex ID: W1972787069 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3999717
@@ Property / cites work: Q3999717 / rank @@
+Normal rank
@@ Property / cites work @@
+Term Rewriting and All That
@@ Property / cites work: Term Rewriting and All That / rank @@
+Normal rank
@@ Property / cites work @@
+Computer proofs in Gödel's class theory with equational definitions for composite and cross
+Normal rank
@@ Property / cites work @@
+On computer-assisted proofs in ordinal number theory
+Normal rank
@@ Property / cites work @@
+Automated Deduction – CADE-19
@@ Property / cites work: Automated Deduction – CADE-19 / rank @@
+Normal rank
@@ Property / cites work @@
+Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
+Normal rank
@@ Property / cites work @@
+Q5809281
@@ Property / cites work: Q5809281 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5765116
@@ Property / cites work: Q5765116 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4790660
@@ Property / cites work: Q4790660 / rank @@
+Normal rank
@@ Property / cites work @@
+Q2757839
@@ Property / cites work: Q2757839 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4272993
@@ Property / cites work: Q4272993 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5661872
@@ Property / cites work: Q5661872 / rank @@
+Normal rank
@@ Property / cites work @@
+An extended arithmetic of ordinal numbers
@@ Property / cites work: An extended arithmetic of ordinal numbers / rank @@
+Normal rank
@@ Property / cites work @@
+What's so special about Kruskal's theorem and the ordinal \(\Gamma{}_ 0\)? A survey of some results in proof theory
+Normal rank
@@ Property / cites work @@
+The consistency of arithmetics
@@ Property / cites work: The consistency of arithmetics / rank @@
+Normal rank
@@ Property / cites work @@
+Q5287513
@@ Property / cites work: Q5287513 / rank @@
+Normal rank
@@ Property / cites work @@
+Set theory. An introduction to independence proofs
+Normal rank
@@ Property / cites work @@
+Partial functions in ACL2
@@ Property / cites work: Partial functions in ACL2 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4818805
@@ Property / cites work: Q4818805 / rank @@
+Normal rank
@@ Property / cites work @@
+Automated Deduction – CADE-19
@@ Property / cites work: Automated Deduction – CADE-19 / rank @@
+Normal rank
@@ Property / cites work @@
+Formal Methods in Computer-Aided Design
@@ Property / cites work: Formal Methods in Computer-Aided Design / rank @@
+Normal rank
@@ Property / cites work @@
+Normal functions and constructive ordinal notations
+Normal rank
@@ Property / cites work @@
+Set theory for verification. I: From foundations to functions
+Normal rank
@@ Property / cites work @@
+Isabelle. A generic theorem prover
@@ Property / cites work: Isabelle. A generic theorem prover / rank @@
+Normal rank
@@ Property / cites work @@
+Set theory for verification. II: Induction and recursion
+Normal rank
@@ Property / cites work @@
+Q4809073
@@ Property / cites work: Q4809073 / rank @@
+Normal rank
@@ Property / cites work @@
+The Relative Consistency of the Axiom of Choice Mechanized Using Isabelle⁄zf
+Normal rank
@@ Property / cites work @@
+Mechanizing set theory. Cardinal arithmetic and the axiom of choice
+Normal rank
@@ Property / cites work @@
+A Mechanically Checked Proof of IEEE Compliance of the Floating Point Multiplication, Division and Square Root Algorithms of the AMD-K7<sup>™</sup> Processor
+Normal rank
@@ Property / cites work @@
+Q4934566
@@ Property / cites work: Q4934566 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4944924
@@ Property / cites work: Q4944924 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4499084
@@ Property / cites work: Q4499084 / rank @@
+Normal rank
@@ Property / cites work @@
+Systems of Logic Based on Ordinals<sup>†</sup>
@@ Property / cites work: Systems of Logic Based on Ordinals<sup>†</sup> / rank @@
+Normal rank