LCF-Style Bit-Blasting in HOL4 (Q3088019): Difference between revisions

@@ 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