From: Lachnitt <lachnitt@stanford.edu>
Date: Wed, 20 Oct 2021 18:50:38 +0000 (-0700)
Subject: [proofs] Alethe: Documentation on Translation (#7394)
X-Git-Tag: cvc5-1.0.0~1040
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5f97877e517f024f6d44d3201f5214853d04cc26;p=cvc5.git

[proofs] Alethe: Documentation on Translation (#7394)

Provides background on the translation into the Alethe calculus that is common to all rules.

Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
---

diff --git a/src/proof/alethe/alethe_post_processor.cpp b/src/proof/alethe/alethe_post_processor.cpp
index 6312f3140..ef7735b44 100644
--- a/src/proof/alethe/alethe_post_processor.cpp
+++ b/src/proof/alethe/alethe_post_processor.cpp
@@ -55,6 +55,79 @@ bool AletheProofPostprocessCallback::update(Node res,
 
   switch (id)
   {
+    // To keep the original shape of the proof node it is necessary to rederive
+    // the original conclusion. However, the term that should be printed might
+    // be different from that conclusion. Thus, it is stored as an additional
+    // argument in the proof node. Usually, the only difference is an additional
+    // cl operator or the outmost or operator being replaced by a cl operator.
+    //
+    // When steps are added to the proof that have not been there previously,
+    // it is unwise to add them in the same manner. To illustrate this the
+    // following counterexample shows the pitfalls of this approach:
+    //
+    //  (or a (or b c))   (not a)
+    // --------------------------- RESOLUTION
+    //  (or b c)
+    //
+    //  is converted into an Alethe proof that should be printed as
+    //
+    //  (cl a (or b c))   (cl (not a))
+    // -------------------------------- RESOLUTION
+    //  (cl (or b c))
+    // --------------- OR
+    //  (cl b c)
+    //
+    // Here, (cl (or b c)) and (cl b c) cannot correspond to the same proof node
+    // (or b c). Thus, we build a new proof node using the kind SEXPR
+    // that is then printed as (cl (or b c)). We denote this wrapping of a proof
+    // node by using an extra pair of parenthesis, i.e. ((or b c)) is the proof
+    // node printed as (cl (or b c)).
+    //
+    //
+    // Some proof rules have a close correspondence in Alethe. There are two
+    // very frequent patterns that, to avoid repetition, are described here and
+    // referred to in the comments on the specific proof rules below.
+    //
+    // The first pattern, which will be called singleton pattern in the
+    // following, adds the original proof node F with the corresponding rule R'
+    // of the Alethe calculus and uses the same premises as the original proof
+    // node (P1:F1) ... (Pn:Fn). However, the conclusion is printed as (cl F).
+    //
+    // This means a cvc5 rule R that looks as follows:
+    //
+    //  (P1:F1) ... (Pn:Fn)
+    // --------------------- R
+    //  F
+    //
+    // is transformed into:
+    //
+    //  (P1:F1) ... (Pn:Fn)
+    // --------------------- R'
+    //  (cl F)*
+    //
+    // * the corresponding proof node is F
+    //
+    // The second pattern, which will be called clause pattern in the following,
+    // has a disjunction (or G1 ... Gn) as conclusion. It also adds the orignal
+    // proof node (or G1 ... Gn) with the corresponding rule R' of the Alethe
+    // calculus and uses the same premises as the original proof node (P1:F1)
+    // ... (Pn:Fn). However, the conclusion is printed as (cl G1 ... Gn), i.e.
+    // the or is replaced by the cl operator.
+    //
+    // This means a cvc5 rule R that looks as follows:
+    //
+    //  (P1:F1) ... (Pn:Fn)
+    // --------------------- R
+    //  (or G1 ... Gn)
+    //
+    // Is transformed into:
+    //
+    //  (P1:F1) ... (Pn:Fn)
+    // --------------------- R'
+    //  (cl G1 ... Gn)*
+    //
+    // * the corresponding proof node is (or G1 ... Gn)
+    //
     //================================================= Core rules
     //======================== Assume and Scope
     case PfRule::ASSUME: