Reconstruction of Z3’s Bit-Vector Proofs in HOL4 and Isabelle/HOL (Q3100212): Difference between revisions

@@ Property / describes a project that uses @@
+HOL-Boogie
@@ Property / describes a project that uses: HOL-Boogie / 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 @@
+z3
@@ Property / describes a project that uses: z3 / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Sledgehammer
@@ Property / describes a project that uses: Sledgehammer / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+CVC Lite
@@ Property / describes a project that uses: CVC Lite / 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 @@
+SMT-LIB
@@ Property / describes a project that uses: SMT-LIB / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+cvc3
@@ Property / describes a project that uses: cvc3 / 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-25379-9_15
+Normal rank
@@ Property / OpenAlex ID @@
+W197756383
@@ Property / OpenAlex ID: W197756383 / rank @@
+Normal rank
@@ Property / cites work @@
+Data compression for proof replay
@@ Property / cites work: Data compression for proof replay / rank @@
+Normal rank
@@ Property / cites work @@
+A Short Presentation of Coq
@@ Property / cites work: A Short Presentation of Coq / rank @@
+Normal rank
@@ Property / cites work @@
+Extending Sledgehammer with SMT Solvers
@@ Property / cites work: Extending Sledgehammer with SMT Solvers / rank @@
+Normal rank
@@ Property / cites work @@
+HOL-Boogie -- an interactive prover-backend for the verifying C compiler
+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 @@
+Tools and Algorithms for the Construction and Analysis of Systems
+Normal rank
@@ Property / cites work @@
+Compression of Propositional Resolution Proofs via Partial Regularization
+Normal rank
@@ Property / cites work @@
+LCF-Style Bit-Blasting in HOL4
@@ Property / cites work: LCF-Style Bit-Blasting in HOL4 / rank @@
+Normal rank
@@ Property / cites work @@
+Edinburgh LCF. A mechanized logic of computation
@@ Property / cites work: Edinburgh LCF. A mechanized logic of computation / rank @@
+Normal rank
@@ Property / cites work @@
+Constructive Type Classes in Isabelle
@@ Property / cites work: Constructive Type Classes in Isabelle / 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 @@
+Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant
+Normal rank
@@ Property / cites work @@
+Q2848688
@@ Property / cites work: Q2848688 / rank @@
+Normal rank
@@ Property / cites work @@
+Efficiently checking propositional refutations in HOL theorem provers
+Normal rank
@@ Property / cites work @@
+Efficiently solving quantified bit-vector formulas
+Normal rank
@@ Property / cites work @@
+Q3624141
@@ Property / cites work: Q3624141 / rank @@
+Normal rank