Modular SMT Proofs for Fast Reflexive Checking Inside Coq (Q3100210): Difference between revisions

@@ Property / describes a project that uses @@
+Coq
@@ Property / describes a project that uses: Coq / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+SIMPLIFY
@@ Property / describes a project that uses: SIMPLIFY / 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 @@
+Metis_
@@ Property / describes a project that uses: Metis_ / 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 @@
+veriT
@@ Property / describes a project that uses: veriT / 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 @@
+cvc3
@@ Property / describes a project that uses: cvc3 / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Gandalf
@@ Property / describes a project that uses: Gandalf / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+Publication
@@ Property / MaRDI profile type: Publication / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1007/978-3-642-25379-9_13
+Normal rank
@@ Property / OpenAlex ID @@
+W92909155
@@ Property / OpenAlex ID: W92909155 / rank @@
+Normal rank
@@ Property / cites work @@
+A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
+Normal rank
@@ Property / cites work @@
+Extending Coq with Imperative Features and Its Application to SAT Verification
+Normal rank
@@ Property / cites work @@
+Fast Reflexive Arithmetic Tactics the Linear Case and Beyond
+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 @@
+Automated Deduction – CADE-20
@@ Property / cites work: Automated Deduction – CADE-20 / rank @@
+Normal rank
@@ Property / cites work @@
+Deciding Effectively Propositional Logic Using DPLL and Substitution Sets
+Normal rank
@@ Property / cites work @@
+Q2848059
@@ Property / cites work: Q2848059 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4809077
@@ Property / cites work: Q4809077 / rank @@
+Normal rank
@@ Property / cites work @@
+Simplify: a theorem prover for program checking
@@ Property / cites work: Simplify: a theorem prover for program checking / rank @@
+Normal rank
@@ Property / cites work @@
+Tools and Algorithms for the Construction and Analysis of Systems
+Normal rank
@@ Property / cites work @@
+A compiled implementation of strong reduction
@@ Property / cites work: A compiled implementation of strong reduction / 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 @@
+Formal certification of a compiler back-end or
@@ Property / cites work: Formal certification of a compiler back-end or / rank @@
+Normal rank
@@ Property / cites work @@
+Q2848688
@@ Property / cites work: Q2848688 / rank @@
+Normal rank
@@ Property / cites work @@
+Q2723407
@@ Property / cites work: Q2723407 / rank @@
+Normal rank
@@ Property / cites work @@
+Simplification by Cooperating Decision Procedures
@@ Property / cites work: Simplification by Cooperating Decision Procedures / rank @@
+Normal rank
@@ Property / cites work @@
+Term Rewriting and Applications
@@ Property / cites work: Term Rewriting and Applications / rank @@
+Normal rank
@@ Property / cites work @@
+Source-Level Proof Reconstruction for Interactive Theorem Proving
+Normal rank
@@ Property / cites work @@
+Q4221106
@@ Property / cites work: Q4221106 / rank @@
+Normal rank
@@ Property / cites work @@
+A Nullstellensatz and a Positivstellensatz in semialgebraic geometry
+Normal rank
@@ Property / cites work @@
+Efficiently checking propositional refutations in HOL theorem provers
+Normal rank
@@ links / mardi / name / links / mardi / name @@
+Publication:3100210