[proofs] Alethe: Translate AND_ELIM rule (#7404)

Implementation of the translation of AND_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 c3925af225a3ae67ee138972c0bd1bb4834be28f..ae67050257801e812c66fd817859e1a6908ddc29 100644 (file)
--- a/src/proof/alethe/alethe_post_processor.cpp
+++ b/src/proof/alethe/alethe_post_processor.cpp
@@ -949,6 +949,17 @@ bool AletheProofPostprocessCallback::update(Node res,
                            {},
                            *cdp);
     }
+    // ======== And elimination
+    // This rule is translated according to the singleton pattern.
+    case PfRule::AND_ELIM:
+    {
+      return addAletheStep(AletheRule::AND,
+                           res,
+                           nm->mkNode(kind::SEXPR, d_cl, res),
+                           children,
+                           {},
+                           *cdp);
+    }
     default:
     {
       return addAletheStep(AletheRule::UNDEFINED,