ACKERMANN’S FUNCTION IN ITERATIVE FORM: A PROOF ASSISTANT EXPERIMENT (Q5037519): Difference between revisions

@@ Property / DOI @@
-.1017/bsl.2021.47
@@ Property / DOI: 10.1017/bsl.2021.47 / rank @@
-Normal rank
@@ Property / author @@
-Lawrence Charles Paulson
@@ Property / author: Lawrence Charles Paulson / rank @@
-Normal rank
@@ Property / author @@
+Lawrence Charles Paulson
@@ Property / author: Lawrence Charles Paulson / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Isabelle/HOL
@@ Property / describes a project that uses: Isabelle/HOL / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+HOL Light
@@ Property / describes a project that uses: HOL Light / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / OpenAlex ID @@
+W3204935188
@@ Property / OpenAlex ID: W3204935188 / rank @@
+Normal rank
@@ Property / cites work @@
+On definitions of constants and types in HOL
@@ Property / cites work: On definitions of constants and types in HOL / rank @@
+Normal rank
@@ Property / cites work @@
+Opinion: The Mechanization of Mathematics
@@ Property / cites work: Opinion: The Mechanization of Mathematics / 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 @@
+Q3893911
@@ Property / cites work: Q3893911 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3753927
@@ Property / cites work: Q3753927 / rank @@
+Normal rank
@@ Property / cites work @@
+Tactics for mechanized reasoning: a commentary on Milner (1984) ‘The use of machines to assist in rigorous proof’
+Normal rank
@@ Property / cites work @@
+Q5812175
@@ Property / cites work: Q5812175 / rank @@
+Normal rank
@@ Property / cites work @@
+Partial and nested recursive function definitions in higher-order logic
+Normal rank
@@ Property / cites work @@
+A consistent foundation for Isabelle/HOL
@@ Property / cites work: A consistent foundation for Isabelle/HOL / rank @@
+Normal rank
@@ Property / cites work @@
+Concrete Semantics
@@ Property / cites work: Concrete Semantics / rank @@
+Normal rank
@@ Property / cites work @@
+Isabelle/HOL. A proof assistant for higher-order logic
+Normal rank
@@ Property / cites work @@
+Q4513619
@@ Property / cites work: Q4513619 / rank @@
+Normal rank
@@ Property / DOI @@
+.1017/BSL.2021.47
@@ Property / DOI: 10.1017/BSL.2021.47 / rank @@
+Normal rank