[proofs] Alethe: Translate CONTRA rule (#7403)

Implementation of the translation of CONTRA 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 dd2927ead840c19053fbb253870d8e6a5246db72..c3925af225a3ae67ee138972c0bd1bb4834be28f 100644 (file)
--- a/src/proof/alethe/alethe_post_processor.cpp
+++ b/src/proof/alethe/alethe_post_processor.cpp
@@ -931,6 +931,24 @@ bool AletheProofPostprocessCallback::update(Node res,
                               {},
                               *cdp);
     }
+    // ======== Contradiction
+    // See proof_rule.h for documentation on the CONTRA rule. This
+    // comment uses variable names as introduced there.
+    //
+    //  P1   P2
+    // --------- RESOLUTION
+    //   (cl)*
+    //
+    // * the corresponding proof node is false
+    case PfRule::CONTRA:
+    {
+      return addAletheStep(AletheRule::RESOLUTION,
+                           res,
+                           nm->mkNode(kind::SEXPR, d_cl),
+                           children,
+                           {},
+                           *cdp);
+    }
     default:
     {
       return addAletheStep(AletheRule::UNDEFINED,