Initial documentation on LFSC (#8365)

diff --git a/docs/proofs/output_alethe.rst b/docs/proofs/output_alethe.rst
index ef3cd3633cc02d1cd5dabf2f69fda21677b8032c..f75cca4912ae20e026ac40505f9f4c692f75e6ca 100644 (file)
--- 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 (file)
index 0000000..3b47e39
--- /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 (file)
index 131a786..0000000
--- 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 04044912de45084e7e7263bf4a30a7a249485ff6..b9089e18bba6fd6063bcdf772f311726c29c2f9e 100644 (file)
--- 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 478b694a0596b37ad3768f56e3cd5f4015be8ac4..78fdda21c9b739ffa242e40a75463e9c988d438d 100644 (file)
--- 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}}
 }
-