diff options
author | Lachnitt <lachnitt@stanford.edu> | 2021-10-25 06:26:40 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-10-25 13:26:40 +0000 |
commit | 418d9264428c56983c92f02537eef321989495b6 (patch) | |
tree | 3a28b7a7bc65e43d05b81491e2b738b7db2d78d3 | |
parent | 6981e3ebde0e65ba772be5cf897611152d1b3ae7 (diff) |
[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>
-rw-r--r-- | src/proof/alethe/alethe_post_processor.cpp | 26 |
1 files changed, 26 insertions, 0 deletions
diff --git a/src/proof/alethe/alethe_post_processor.cpp b/src/proof/alethe/alethe_post_processor.cpp index 920ca7dcb..7acdbfffe 100644 --- 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, |