diff options
author | Lachnitt <lachnitt@stanford.edu> | 2021-10-26 04:46:26 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-10-26 11:46:26 +0000 |
commit | 3735b033da730f532de39af4c069f3a0d00e6484 (patch) | |
tree | b500021a1e5f156c740a15aaa142cd16c1321623 | |
parent | 446185d47831197312d6a95fc78a89ce4bbe6f9c (diff) |
[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>
-rw-r--r-- | src/proof/alethe/alethe_post_processor.cpp | 22 |
1 files changed, 22 insertions, 0 deletions
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, |