From 2b2ccd57aed86414a6cee5251e3b55aeafd256e3 Mon Sep 17 00:00:00 2001 From: Lachnitt Date: Tue, 26 Oct 2021 06:21:26 -0700 Subject: [PATCH] [proofs] Alethe: Translate CONTRA rule (#7403) Implementation of the translation of CONTRA rules into the Alethe calculus. Co-authored-by: Haniel Barbosa --- src/proof/alethe/alethe_post_processor.cpp | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/src/proof/alethe/alethe_post_processor.cpp b/src/proof/alethe/alethe_post_processor.cpp index dd2927ead..c3925af22 100644 --- 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, -- 2.30.2