From 2a5d89da3be4e4b807d9336e6c560997035b5089 Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Fri, 1 Apr 2022 14:27:05 -0300 Subject: [PATCH] [proofs] [doc] Minor changes to general proofs page, some changes to Alethe page, added DOT page (#8501) --- docs/proofs/output_alethe.rst | 20 +++++- docs/proofs/output_dot.rst | 8 +++ docs/proofs/proofs.rst | 16 +++-- docs/references.bib | 112 ++++++++++++++++++++++++++++++++-- 4 files changed, 142 insertions(+), 14 deletions(-) create mode 100644 docs/proofs/output_dot.rst diff --git a/docs/proofs/output_alethe.rst b/docs/proofs/output_alethe.rst index f75cca491..937d7d1d4 100644 --- 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 `, cvc5 outputs proofs in the `Alethe proof format `_. +Using the flag :ref:`proof-format-mode=alethe `, +cvc5 outputs proofs in the `Alethe proof format +`_. Additonally, the +following additional flags are currently required: :ref:`simplification=none +`, :ref:`dag-thresh=0 `, +:ref:`proof-granularity=theory-rewrite `. 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 ` :ref:`--dag-thresh=0 `. +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 `_. -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 index 000000000..30665cd72 --- /dev/null +++ b/docs/proofs/output_dot.rst @@ -0,0 +1,8 @@ +Proof format: DOT +================= + +Using the flag :ref:`proof-format-mode=dot `, cvc5 outputs proofs in the DOT format. + +The DOT format is a graph description language (see e.g. a description `here `_.). 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 `_. 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 b9089e18b..face73c30 100644 --- 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 +`. + +Optionally cvc5 can convert and output its internal proofs into the following +external formats: .. toctree:: :maxdepth: 1 - + Alethe - Lean LFSC + DOT - -some other stuff: :doc:`proof rules `. +where note that the DOT format is only meant for visualization. diff --git a/docs/references.bib b/docs/references.bib index 78fdda21c..35224aa51 100644 --- 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 -- 2.30.2