diff options
| -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, |