The reflective Milawa theorem prover is sound (down to the machine code that runs it) (Q286790): Difference between revisions

@@ Property / Mathematics Subject Classification ID @@
+T15
@@ Property / Mathematics Subject Classification ID: 68T15 / rank @@
+Normal rank
@@ Property / zbMATH DE Number @@
+6585237
@@ Property / zbMATH DE Number: 6585237 / rank @@
+Normal rank
@@ Property / zbMATH Keywords @@
+soundness
@@ Property / zbMATH Keywords: soundness / rank @@
+Normal rank
@@ Property / zbMATH Keywords @@
+theorem proving
@@ Property / zbMATH Keywords: theorem proving / rank @@
+Normal rank
@@ Property / zbMATH Keywords @@
+proof assistant
@@ Property / zbMATH Keywords: proof assistant / rank @@
+Normal rank
@@ Property / zbMATH Keywords @@
+machine code
@@ Property / zbMATH Keywords: machine code / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+ACL2
@@ Property / describes a project that uses: ACL2 / 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 @@
+HOL
@@ Property / describes a project that uses: HOL / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+CakeML
@@ Property / describes a project that uses: CakeML / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+OpenTheory
@@ Property / describes a project that uses: OpenTheory / 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 @@
+Isabelle/HOL
@@ Property / describes a project that uses: Isabelle/HOL / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+z3
@@ Property / describes a project that uses: z3 / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+HOL Light
@@ Property / describes a project that uses: HOL Light / 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 @@
+Ivy
@@ Property / describes a project that uses: Ivy / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Jitawa
@@ Property / describes a project that uses: Jitawa / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+DRAT-trim
@@ Property / describes a project that uses: DRAT-trim / 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-015-9324-6
+Normal rank
@@ Property / OpenAlex ID @@
+W1904308182
@@ Property / OpenAlex ID: W1904308182 / rank @@
+Normal rank
@@ links / mardi / name / links / mardi / name @@
+Publication:286790