[proofs] Alethe: Translate SPLIT rule (#7399)

Implementation of the translation of SPLIT 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 920ca7dcb84045b0b24af5d82c70430c2d93c37a..7acdbfffea5ed5c07b20ddcc26a5807949ddbc76 100644 (file)
--- a/src/proof/alethe/alethe_post_processor.cpp
+++ b/src/proof/alethe/alethe_post_processor.cpp
@@ -760,6 +760,32 @@ bool AletheProofPostprocessCallback::update(Node res,
                            {},
                            *cdp);
     }
+    // ======== Split
+    // See proof_rule.h for documentation on the SPLIT rule. This comment
+    // uses variable names as introduced there.
+    //
+    // --------- NOT_NOT      --------- NOT_NOT
+    //    VP1                    VP2
+    // -------------------------------- RESOLUTION
+    //          (cl F (not F))*
+    //
+    // VP1: (cl (not (not (not F))) F)
+    // VP2: (cl (not (not (not (not F)))) (not F))
+    //
+    // * the corresponding proof node is (or F (not F))
+    case PfRule::SPLIT:
+    {
+      Node vp1 = nm->mkNode(
+          kind::SEXPR, d_cl, args[0].notNode().notNode().notNode(), args[0]);
+      Node vp2 = nm->mkNode(kind::SEXPR,
+                              d_cl,
+                              args[0].notNode().notNode().notNode().notNode(),
+                              args[0].notNode());
+
+      return addAletheStep(AletheRule::NOT_NOT, vp2, vp2, {}, {}, *cdp)
+          && addAletheStep(AletheRule::NOT_NOT, vp1, vp1, {}, {}, *cdp)
+          && addAletheStepFromOr(AletheRule::RESOLUTION, res, {vp1, vp2}, {}, *cdp);
+    }
     default:
     {
       return addAletheStep(AletheRule::UNDEFINED,