LCF-Style Bit-Blasting in HOL4 (Q3088019): 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 @@
+z3
@@ Property / describes a project that uses: z3 / 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/978-3-642-22863-6_26
+Normal rank
@@ Property / OpenAlex ID @@
+W2165236431
@@ Property / OpenAlex ID: W2165236431 / rank @@
+Normal rank
@@ Property / cites work @@
+Efficiently checking propositional refutations in HOL theorem provers
+Normal rank
@@ Property / cites work @@
+Fast LCF-Style Proof Reconstruction for Z3
@@ Property / cites work: Fast LCF-Style Proof Reconstruction for Z3 / rank @@
+Normal rank
@@ Property / cites work @@
+Deciding Bit-Vector Arithmetic with Abstraction
@@ Property / cites work: Deciding Bit-Vector Arithmetic with Abstraction / rank @@
+Normal rank
@@ Property / cites work @@
+Theorem Proving in Higher Order Logics
@@ Property / cites work: Theorem Proving in Higher Order Logics / rank @@
+Normal rank
@@ Property / cites work @@
+A Verified Runtime for a Verified Theorem Prover
@@ Property / cites work: A Verified Runtime for a Verified Theorem Prover / rank @@
+Normal rank