Disprover should report needed hypotheses back to Rodin
Description
Environment
None
Gliffy Diagrams
Activity
Show:
Details
Details
Assignee
Sebastian Krings
Sebastian KringsReporter
Sebastian Krings
Sebastian KringsPriority
MajorCreated June 4, 2014 at 10:37 AM
Updated June 4, 2014 at 10:37 AM
Currently, when the Disprover is able to discharge a proof obligation, we do not submit which hypotheses were used:
return ProverFactory.makeProofRule(this, input, sequent.goal(),
null, IConfidence.DISCHARGED_MAX,
"ProB (no enumeration / all cases checked)");
We should replace "null" by a set of predicates used to discharge the po. That way, Rodin would be able to replay to proof if the model changes and it is still applicable.