From: Lachnitt <lachnitt@stanford.edu>
Date: Tue, 26 Oct 2021 11:46:26 +0000 (-0700)
Subject: [proofs] Alethe: Translate NOT_NOT_ELIM rule (#7402)
X-Git-Tag: cvc5-1.0.0~976
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3735b033da730f532de39af4c069f3a0d00e6484;p=cvc5.git

[proofs] Alethe: Translate NOT_NOT_ELIM rule (#7402)

Implementation of the translation of NOT_NOT_ELIM rules into the Alethe calculus.

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 167b885f4..dd2927ead 100644
--- a/src/proof/alethe/alethe_post_processor.cpp
+++ b/src/proof/alethe/alethe_post_processor.cpp
@@ -909,6 +909,28 @@ bool AletheProofPostprocessCallback::update(Node res,
                               {},
                               *cdp);
     }
+    // ======== Double negation elimination
+    // See proof_rule.h for documentation on the NOT_NOT_ELIM rule. This comment
+    // uses variable names as introduced there.
+    //
+    // ---------------------------------- NOT_NOT
+    //  (VP1:(cl (not (not (not F))) F))           (P:(not (not F)))
+    // ------------------------------------------------------------- RESOLUTION
+    //                            (cl F)*
+    //
+    // * the corresponding proof node is F
+    case PfRule::NOT_NOT_ELIM:
+    {
+      Node vp1 = nm->mkNode(kind::SEXPR, d_cl, children[0].notNode(), res);
+
+      return addAletheStep(AletheRule::NOT_NOT, vp1, vp1, {}, {}, *cdp)
+             && addAletheStep(AletheRule::RESOLUTION,
+                              res,
+                              nm->mkNode(kind::SEXPR, d_cl, res),
+                              {vp1, children[0]},
+                              {},
+                              *cdp);
+    }
     default:
     {
       return addAletheStep(AletheRule::UNDEFINED,