A verified SAT solver framework with learn, forget, restart, and incrementality (Q1663234): Difference between revisions

@@ Property / describes a project that uses @@
+VAMPIRE
@@ Property / describes a project that uses: VAMPIRE / 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 @@
+Imperative Refinement
@@ Property / describes a project that uses: Imperative Refinement / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Chaff
@@ Property / describes a project that uses: Chaff / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Autoref
@@ Property / describes a project that uses: Autoref / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+DPT
@@ Property / describes a project that uses: DPT / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Completeness theorem
@@ Property / describes a project that uses: Completeness theorem / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+SAT Solver Verification
@@ Property / describes a project that uses: SAT Solver Verification / 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 @@
+versat
@@ Property / describes a project that uses: versat / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Isar
@@ Property / describes a project that uses: Isar / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+MiniSat
@@ Property / describes a project that uses: MiniSat / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Locales
@@ Property / describes a project that uses: Locales / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+IsaFoL
@@ Property / describes a project that uses: IsaFoL / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+AVATAR
@@ Property / describes a project that uses: AVATAR / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Archive Formal Proofs
@@ Property / describes a project that uses: Archive Formal Proofs / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / OpenAlex ID @@
+W2790974881
@@ Property / OpenAlex ID: W2790974881 / rank @@
+Normal rank
@@ Property / Wikidata QID @@
+Q64950500
@@ Property / Wikidata QID: Q64950500 / rank @@
+Normal rank
@@ Property / cites work @@
+Q2751353
@@ Property / cites work: Q2751353 / rank @@
+Normal rank
@@ Property / cites work @@
+Locales: a module system for mathematical theories
+Normal rank
@@ Property / cites work @@
+Q5503674
@@ Property / cites work: Q5503674 / 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 @@
+Automatic Proof and Disproof in Isabelle/HOL
@@ Property / cites work: Automatic Proof and Disproof in Isabelle/HOL / rank @@
+Normal rank
@@ Property / cites work @@
+Mechanizing the Metatheory of Sledgehammer
@@ Property / cites work: Mechanizing the Metatheory of Sledgehammer / rank @@
+Normal rank
@@ Property / cites work @@
+Semi-intelligible Isar proofs from machine-generated proofs
+Normal rank
@@ Property / cites work @@
+A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality
+Normal rank
@@ Property / cites work @@
+Soundness and completeness proofs by coinductive methods
+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 @@
+Imperative Functional Programming with Isabelle/HOL
+Normal rank
@@ Property / cites work @@
+Efficient certified RAT verification
@@ Property / cites work: Efficient certified RAT verification / rank @@
+Normal rank
@@ Property / cites work @@
+A machine program for theorem-proving
@@ Property / cites work: A machine program for theorem-proving / rank @@
+Normal rank
@@ Property / cites work @@
+Theory and Applications of Satisfiability Testing
@@ Property / cites work: Theory and Applications of Satisfiability Testing / rank @@
+Normal rank
@@ Property / cites work @@
+versat: A Verified Modern SAT Solver
@@ Property / cites work: versat: A Verified Modern SAT Solver / rank @@
+Normal rank
@@ Property / cites work @@
+Teaching Semantics with a Proof Assistant: No More LSD Trip Proofs
+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 @@
+Code Generation via Higher-Order Rewrite Systems
@@ Property / cites work: Code Generation via Higher-Order Rewrite Systems / rank @@
+Normal rank
@@ Property / cites work @@
+Q4247076
@@ Property / cites work: Q4247076 / rank @@
+Normal rank
@@ Property / cites work @@
+Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL
+Normal rank
@@ Property / cites work @@
+Partial Recursive Functions in Higher-Order Logic
@@ Property / cites work: Partial Recursive Functions in Higher-Order Logic / rank @@
+Normal rank
@@ Property / cites work @@
+Architecting Solvers for SAT Modulo Theories: Nelson-Oppen with DPLL
+Normal rank
@@ Property / cites work @@
+Optimal speedup of Las Vegas algorithms
@@ Property / cites work: Optimal speedup of Las Vegas algorithms / rank @@
+Normal rank
@@ Property / cites work @@
+Automatic Data Refinement
@@ Property / cites work: Automatic Data Refinement / rank @@
+Normal rank
@@ Property / cites work @@
+Refinement to Imperative/HOL
@@ Property / cites work: Refinement to Imperative/HOL / rank @@
+Normal rank
@@ Property / cites work @@
+Efficient verified (UN)SAT certificate checking
@@ Property / cites work: Efficient verified (UN)SAT certificate checking / rank @@
+Normal rank
@@ Property / cites work @@
+Formalization of Abstract State Transition Systems for SAT
+Normal rank
@@ Property / cites work @@
+Solving SAT and SAT Modulo Theories
@@ Property / cites work: Solving SAT and SAT Modulo Theories / 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 @@
+Formalization of the Resolution Calculus for First-Order Logic
+Normal rank
@@ Property / cites work @@
+Metamathematics, Machines and Gödel's Proof
@@ Property / cites work: Metamathematics, Machines and Gödel's Proof / rank @@
+Normal rank
@@ Property / cites work @@
+The Mechanical Verification of a DPLL-Based Satisfiability Solver
+Normal rank
@@ Property / cites work @@
+AVATAR: The Architecture for First-Order Theorem Provers
+Normal rank
@@ Property / cites work @@
+Automated Reasoning Building Blocks
@@ Property / cites work: Automated Reasoning Building Blocks / rank @@
+Normal rank
@@ Property / cites work @@
+Program development by stepwise refinement
@@ Property / cites work: Program development by stepwise refinement / rank @@
+Normal rank