From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 23 Mar 2022 02:12:34 +0000 (-0500)
Subject: Initial documentation on LFSC (#8365)
X-Git-Tag: cvc5-1.0.0~202
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7d0696aa839f39fa3f262317d780594841edb30e;p=cvc5.git

Initial documentation on LFSC (#8365)
---

diff --git a/docs/proofs/output_alethe.rst b/docs/proofs/output_alethe.rst
index ef3cd3633..f75cca491 100644
--- a/docs/proofs/output_alethe.rst
+++ b/docs/proofs/output_alethe.rst
@@ -1,7 +1,7 @@
 Proof format: Alethe
 ====================
 
-Using the flag :ref:`--proof-format-mode=alethe <lbl-option-proof-format-mode>`, cvc5 can output 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 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>`.
 
diff --git a/docs/proofs/output_lfsc.rst b/docs/proofs/output_lfsc.rst
new file mode 100644
index 000000000..3b47e3962
--- /dev/null
+++ b/docs/proofs/output_lfsc.rst
@@ -0,0 +1,14 @@
+Proof format: LFSC
+==================
+
+Using the flag :ref:`proof-format-mode=lfsc <lbl-option-proof-format-mode>`, cvc5 outputs proofs in the LFSC proof format.
+
+The LFSC proof format is based on the LF logical framework extended with computational side conditions, as described in :cite:`DBLP:journals/fmsd/StumpORHT13`. A high performance C++ proof checker for LFSC is available `here <https://github.com/cvc5/LFSC>`_.
+
+For a quick start, the cvc5 repository contains a :cvc5repo:`script <contrib/get-lfsc-checker>` which will download and install the LFSC proof checker, and create scripts for generating proofs with cvc5 and checking them with the LFSC proof checker.
+
+LFSC is a meta-framework, meaning that the proof rules used by cvc5 are defined in signature files, also contained within the cvc5 repository in this :cvc5repo:`directory <proofs/lfsc/signatures>`. Based on these signatures, cvc5 provides basic support for LFSC proofs over all theories that it supports.
+
+Note that several proof rules in the internal calculus are not yet supported in LFSC signatures, and are instead printed as `trust` steps in the LFSC proof. A trust step proves an arbitrary formula with no provided justification. The LFSC proof contains warnings for which proof rules from the internal calculus were recorded as trust steps in the LFSC proof.
+
+For more fine-grained proofs, the additional option :ref:`proof-granularity=theory-rewrite <lbl-option-proof-granularity>` should be passed to cvc5. This often will result in LFSC proofs with more detail, and whose trust steps correspond only to equalities corresponding to theory rewrites.
diff --git a/docs/proofs/output_lsfc.rst b/docs/proofs/output_lsfc.rst
deleted file mode 100644
index 131a7864d..000000000
--- a/docs/proofs/output_lsfc.rst
+++ /dev/null
@@ -1,2 +0,0 @@
-Proof format: LSFC
-==================
\ No newline at end of file
diff --git a/docs/proofs/proofs.rst b/docs/proofs/proofs.rst
index 04044912d..b9089e18b 100644
--- a/docs/proofs/proofs.rst
+++ b/docs/proofs/proofs.rst
@@ -8,7 +8,7 @@ cvc5 can generate formal proofs and output it in the following formats:
    
    Alethe <output_alethe>
    Lean <output_lean>
-   LSFC <output_lsfc>
+   LFSC <output_lfsc>
 
 
-some other stuff: :doc:`proof rules <proof_rules>`.
\ No newline at end of file
+some other stuff: :doc:`proof rules <proof_rules>`.
diff --git a/docs/references.bib b/docs/references.bib
index 478b694a0..78fdda21c 100644
--- a/docs/references.bib
+++ b/docs/references.bib
@@ -120,6 +120,24 @@
   bibsource = {dblp computer science bibliography, https://dblp.org}
 }
 
+@article{DBLP:journals/fmsd/StumpORHT13,
+  author    = {Aaron Stump and
+               Duckki Oe and
+               Andrew Reynolds and
+               Liana Hadarean and
+               Cesare Tinelli},
+  title     = {{SMT} proof checking using a logical framework},
+  journal   = {Formal Methods Syst. Des.},
+  volume    = {42},
+  number    = {1},
+  pages     = {91--118},
+  year      = {2013},
+  url       = {https://doi.org/10.1007/s10703-012-0163-3},
+  doi       = {10.1007/s10703-012-0163-3},
+  timestamp = {Tue, 27 Jul 2021 08:54:10 +0200},
+  biburl    = {https://dblp.org/rec/journals/fmsd/StumpORHT13.bib},
+  bibsource = {dblp computer science bibliography, https://dblp.org}
+}
 
 @TECHREPORT{BarFT-RR-17,
   author =	 {Clark Barrett and Pascal Fontaine and Cesare Tinelli},
@@ -128,4 +146,3 @@
   year =	 2017,
   note =	 {Available at {\tt www.SMT-LIB.org}}
 }
-