diff options
author | Lachnitt <lachnitt@stanford.edu> | 2021-10-26 06:21:26 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-10-26 13:21:26 +0000 |
commit | 2b2ccd57aed86414a6cee5251e3b55aeafd256e3 (patch) | |
tree | 1afa8710b522969d21af305fd7ee6cb6cfb6e21c | |
parent | 396dfa071d5ab40a1d2ab3ab84c5fdf41c3affd9 (diff) |
[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>
-rw-r--r-- | src/proof/alethe/alethe_post_processor.cpp | 18 |
1 files changed, 18 insertions, 0 deletions
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, |