[proofs] [doc] Minor changes to general proofs page, some changes to Alethe page...

diff --git a/docs/proofs/output_alethe.rst b/docs/proofs/output_alethe.rst
index f75cca4912ae20e026ac40505f9f4c692f75e6ca..937d7d1d480e706136ac76d15616be1da21c8e6d 100644 (file)
--- a/docs/proofs/output_alethe.rst
+++ b/docs/proofs/output_alethe.rst
@@ -1,8 +1,22 @@
 Proof format: Alethe
 ====================
 
-Using the flag :ref:`proof-format-mode=alethe <lbl-option-proof-format-mode>`, cvc5 outputs proofs in the `Alethe proof format <https://verit.loria.fr/documentation/alethe-spec.pdf>`_.
+Using the flag :ref:`proof-format-mode=alethe <lbl-option-proof-format-mode>`,
+cvc5 outputs proofs in the `Alethe proof format
+<https://verit.loria.fr/documentation/alethe-spec.pdf>`_. Additonally, the
+following additional flags are currently required: :ref:`simplification=none
+<lbl-option-simplification>`, :ref:`dag-thresh=0 <lbl-option-dag-thresh>`,
+:ref:`proof-granularity=theory-rewrite <lbl-option-proof-granularity>`. These requirements are due to not yet
+supporting printing proofs with term sharing and proofs with non-detailed steps.
 
-Additonally, the following flags should be used to produce proofs without term sharing (which is not supported for the Alethe backend yet): :ref:`--simplification=none <lbl-option-simplification>` :ref:`--dag-thresh=0 <lbl-option-dag-thresh>`.
+The Alethe proof format is a flexible proof format for SMT solvers based on
+SMT-LIB.  It includes both coarse- and fine-grained steps and was first
+implemented in the veriT solver :cite:`Bouton2009`.  Alethe proofs can be
+checked via reconstruction within Isabelle/HOL :cite:`Barbosa2020, Schurr2021`
+as well as within Coq, the latter via the SMTCoq plugin :cite:`Armand2011,
+Ekici2017`. There is also a high performance Rust proof checker for Alethe,
+available `here <https://github.com/ufmg-smite/alethe-proof-checker>`_.
 
-Currently, only the theory of equality with uninterpreted functions, parts of the theory of arithmetic and parts of the theory of quantifiers are supported.
+Currently, only the theory of equality with uninterpreted functions, parts of
+the theory of arithmetic and parts of the theory of quantifiers are supported in
+cvc5's Alethe proofs.

diff --git a/docs/proofs/output_dot.rst b/docs/proofs/output_dot.rst
new file mode 100644 (file)
index 0000000..30665cd
--- /dev/null
+++ b/docs/proofs/output_dot.rst
@@ -0,0 +1,8 @@
+Proof format: DOT
+=================
+
+Using the flag :ref:`proof-format-mode=dot <lbl-option-proof-format-mode>`, cvc5 outputs proofs in the DOT format.
+
+The DOT format is a graph description language (see e.g. a description `here <https://en.wikipedia.org/wiki/DOT_(graph_description_language)>`_.). It can be used, among other things, for visualization.
+
+We leverage this format for visualizing cvc5 proofs, in the internal calculus, as a graph. One can use a default dot visualizer or the dedicated proof visualizer available `here <https://ufmg-smite.github.io/proof-visualizer>`_. It suffices to upload the DOT proof outputted by cvc5, saved into a file. The visualizer offers several custom features, such as fold/unfold subproofs, coloring nodes, and stepwise expansion of let terms.

diff --git a/docs/proofs/proofs.rst b/docs/proofs/proofs.rst
index b9089e18bba6fd6063bcdf772f311726c29c2f9e..face73c30f22011aa0235d5fdf144f57283052a9 100644 (file)
--- a/docs/proofs/proofs.rst
+++ b/docs/proofs/proofs.rst
@@ -1,14 +1,18 @@
-Proof generation
+Proof production
 ================
 
-cvc5 can generate formal proofs and output it in the following formats:
+cvc5 produces proofs in an internal proof calculus that faithfully reflects its
+reasoning. Here is a comprehensive description of the :doc:`proof rules
+<proof_rules>`.
+
+Optionally cvc5 can convert and output its internal proofs into the following
+external formats:
 
 .. toctree::
    :maxdepth: 1
-   
+
    Alethe <output_alethe>
-   Lean <output_lean>
    LFSC <output_lfsc>
+   DOT <output_dot>
 
-
-some other stuff: :doc:`proof rules <proof_rules>`.
+where note that the DOT format is only meant for visualization.

diff --git a/docs/references.bib b/docs/references.bib
index 78fdda21c9b739ffa242e40a75463e9c988d438d..35224aa5162b1a5dda8134e8ccd773de0b7f0e4d 100644 (file)
--- a/docs/references.bib
+++ b/docs/references.bib
@@ -1,3 +1,9 @@
+@string{cade   = "Conference on Automated Deduction (CADE)"}
+@string{cpp = "Certified Programs and Proofs (CPP)"}
+@string{cav    = "Computer Aided Verification (CAV)"}
+@string{jar    = "Journal of Automated Reasoning"}
+@string{lncs   = "Lecture Notes in Computer Science"}
+
 @article{DBLP:journals/tocl/CimattiGIRS18,
   author    = {Alessandro Cimatti and
                Alberto Griggio and
@@ -140,9 +146,105 @@
 }
 
 @TECHREPORT{BarFT-RR-17,
-  author =      {Clark Barrett and Pascal Fontaine and Cesare Tinelli},
-  title =       {{The SMT-LIB Standard: Version 2.6}},
-  institution =         {Department of Computer Science, The University of Iowa},
-  year =        2017,
-  note =        {Available at {\tt www.SMT-LIB.org}}
+  author =   {Clark Barrett and Pascal Fontaine and Cesare Tinelli},
+  title =  {{The SMT-LIB Standard: Version 2.6}},
+  institution =  {Department of Computer Science, The University of Iowa},
+  year =   2017,
+  note =   {Available at {\tt www.SMT-LIB.org}}
+}
+
+@inproceedings{Bouton2009,
+  author    = {Thomas Bouton and
+               Diego Caminha B. de Oliveira and
+               David D{\'{e}}harbe and
+               Pascal Fontaine},
+  title     = {{veriT}: {A}n {O}pen, {T}rustable and {E}fficient {SMT-S}olver},
+  booktitle = cade,
+  pages     = {151--156},
+  year      = {2009},
+  url       = {http://dx.doi.org/10.1007/978-3-642-02959-2_12},
+  doi       = {10.1007/978-3-642-02959-2_12},
+  editor    = {Renate A. Schmidt},
+  series    = lncs,
+  volume    = {5663},
+  publisher = {Springer},
 }
+
+@inproceedings{Armand2011,
+  author    = {Micha{\"e}l Armand and
+               Germain Faure and
+               Benjamin Gr{\'e}goire and
+               Chantal Keller and
+               Laurent Th{\'e}ry and
+               Benjamin Werner},
+  title     = {A~Modular Integration of {SAT}\slash{SMT} Solvers to {Coq} through
+               Proof Witnesses},
+  booktitle = cpp,
+  pages     = {135--150},
+  editor    = {Jean-Pierre Jouannaud and
+               Zhong Shao},
+  publisher = {Springer},
+  series    = lncs,
+  volume    = {7086},
+  year      = {2011},
+  doi       = {10.1007/978-3-642-25379-9_12}
+}
+
+@inproceedings{Ekici2017,
+  author    = {Burak Ekici and
+               Alain Mebsout and
+               Cesare Tinelli and
+               Chantal Keller and
+               Guy Katz and
+               Andrew Reynolds and
+               Clark W. Barrett},
+  title     = {SMTCoq: {A} Plug-In for Integrating {SMT} Solvers into Coq},
+  booktitle = cav,
+  pages     = {126--133},
+  year      = {2017},
+  url       = {https://doi.org/10.1007/978-3-319-63390-9_7},
+  doi       = {10.1007/978-3-319-63390-9_7},
+  editor    = {Rupak Majumdar and
+               Viktor Kuncak},
+  series    = lncs,
+  volume    = {10427},
+  publisher = {Springer},
+}
+
+@article{Barbosa2020,
+  author    = {Haniel Barbosa and
+               Jasmin Christian Blanchette and
+               Mathias Fleury and
+               Pascal Fontaine},
+  title     = {Scalable Fine-Grained Proofs for Formula Processing},
+  journal   = jar,
+  volume    = {64},
+  number    = {3},
+  pages     = {485--510},
+  year      = {2020},
+  url       = {https://doi.org/10.1007/s10817-018-09502-y},
+  doi       = {10.1007/s10817-018-09502-y},
+  timestamp = {Thu, 19 Mar 2020 10:23:41 +0100},
+  biburl    = {https://dblp.org/rec/journals/jar/BarbosaBFF20.bib},
+  bibsource = {dblp computer science bibliography, https://dblp.org}
+}
+
+@inproceedings{Schurr2021,
+  author    = {Hans{-}J{\"{o}}rg Schurr and
+               Mathias Fleury and
+               Martin Desharnais},
+  editor    = {Andr{\'{e}} Platzer and
+               Geoff Sutcliffe},
+  title     = {Reliable Reconstruction of Fine-grained Proofs in a Proof Assistant},
+  booktitle = cade,
+  series    = lncs,
+  volume    = {12699},
+  pages     = {450--467},
+  publisher = {Springer},
+  year      = {2021},
+  url       = {https://doi.org/10.1007/978-3-030-79876-5\_26},
+  doi       = {10.1007/978-3-030-79876-5\_26},
+  timestamp = {Mon, 12 Jul 2021 14:18:46 +0200},
+  biburl    = {https://dblp.org/rec/conf/cade/SchurrFD21.bib},
+  bibsource = {dblp computer science bibliography, https://dblp.org}
+}
\ No newline at end of file