diff options
| author | Lachnitt <lachnitt@stanford.edu> | 2021-10-25 15:24:04 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-10-25 22:24:04 +0000 |
| commit | 446185d47831197312d6a95fc78a89ce4bbe6f9c (patch) | |
| tree | cea8055d184ad44ac8b4695bedfe49eb38f4fbb6 | |
| parent | cb748679157eb658ce5d1173d8f26957daf8f3df (diff) | |
[proofs] Alethe: Translate MODUS_PONENS rule (#7401)
Implementation of the translation of MODUS_PONENS rules into the Alethe calculus.
Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
| -rw-r--r-- | src/proof/alethe/alethe_post_processor.cpp | 24 |
1 files changed, 24 insertions, 0 deletions
diff --git a/src/proof/alethe/alethe_post_processor.cpp b/src/proof/alethe/alethe_post_processor.cpp index 6aa6498f6..167b885f4 100644 --- a/src/proof/alethe/alethe_post_processor.cpp +++ b/src/proof/alethe/alethe_post_processor.cpp @@ -885,6 +885,30 @@ bool AletheProofPostprocessCallback::update(Node res, {}, *cdp); } + // ======== Modus ponens + // See proof_rule.h for documentation on the MODUS_PONENS rule. This comment + // uses variable names as introduced there. + // + // (P2:(=> F1 F2)) + // ------------------------ IMPLIES + // (VP1:(cl (not F1) F2)) (P1:F1) + // -------------------------------------------- RESOLUTION + // (cl F2)* + // + // * the corresponding proof node is F2 + case PfRule::MODUS_PONENS: + { + Node vp1 = nm->mkNode(kind::SEXPR, d_cl, children[0].notNode(), res); + + return addAletheStep( + AletheRule::IMPLIES, vp1, vp1, {children[1]}, {}, *cdp) + && addAletheStep(AletheRule::RESOLUTION, + res, + nm->mkNode(kind::SEXPR, d_cl, res), + {vp1, children[0]}, + {}, + *cdp); + } default: { return addAletheStep(AletheRule::UNDEFINED, |