1 files changed, 38 insertions, 0 deletions
diff --git a/content/zettel/3d2b.md b/content/zettel/3d2b.md
new file mode 100644
index 0000000..f4898aa
--- /dev/null
+++ b/content/zettel/3d2b.md
@@ -0,0 +1,38 @@
++++
+title = "SMTCoq as a formalisation in Coq"
+date = "2022-08-02"
+author = "Yann Herklotz"
+tags = []
+categories = []
+backlinks = ["3d2a"]
+forwardlinks = ["3d2b1"]
+zettelid = "3d2b"
++++
+
+SMTCoq \[1\] is a tool that formalises these rewriting traces in Coq, so
+that traces from various tools (veriT, cvc4 and zchaff) can be read and
+then checked according to the input formula. This actually does not
+require any trust in the parsing and pretty printing to pass the input
+to the SAT solver, because the initial formula is already represented in
+Coq, then the trace will also be represented in Coq, and so the checker
+can just check that this arbitrary trace present in Coq does indeed
+simplify the formula to $\perp$.
+
+<div id="refs" class="references csl-bib-body" markdown="1">
+
+<div id="ref-armand11_modul_integ_sat_smt_solver" class="csl-entry"
+markdown="1">
+
+<span class="csl-left-margin">\[1\]
+</span><span class="csl-right-inline">M. Armand, G. Faure, B. Grégoire,
+C. Keller, L. Théry, and B. Werner, “A modular integration of SAT/SMT
+solvers to coq through proof witnesses,” in *Certified programs and
+proofs*, J.-P. Jouannaud and Z. Shao, Eds., Berlin, Heidelberg: Springer
+Berlin Heidelberg, 2011, pp. 135–150. doi:
+[10.1007/978-3-642-25379-9_12].</span>
+
+</div>
+
+</div>
+
+  [10.1007/978-3-642-25379-9_12]: https://doi.org/10.1007/978-3-642-25379-9_12