public class ProofExplorationService
extends java.lang.Object
The branch not corresponding to the desried change is set to interactive. This enables that the automatic strategies avoid expanding this branch and the user needs to activate the branch by hand.
Adding formulas to the antecedent: '==> p' as goal node and adding q to the antecedent results in two branches:
1) q ==> p 2) ==> p,q <-- this branch is set to interactive such that the automatic strategies do not expand it Adding formulas to the succedent: '==> p' as goal node and adding q to the succedent results in two branches:
1) q ==> p <-- this branch is set to interactive such that the automatic strategies do not expand it 2) ==> p,q
Constructor and Description |
---|
ProofExplorationService(Proof proof,
Services services) |
Modifier and Type | Method and Description |
---|---|
Node |
applyChangeFormula(Goal g,
PosInOccurrence pio,
Term term,
Term newTerm) |
static ProofExplorationService |
get(KeYMediator mediator) |
Taclet |
getCutTaclet()
Finds the `cut` taclet in the current proof environment.
|
Node |
soundAddition(Goal g,
Term t,
boolean antecedent)
Create a new Tacletapp that add a formula to the sequent using the cut rule and disabeling one of the branches
|
void |
soundHide(Goal g,
PosInOccurrence pio,
Term term) |
@Nonnull public static ProofExplorationService get(KeYMediator mediator)
@Nonnull public Taclet getCutTaclet()
@Nonnull public Node soundAddition(@Nonnull Goal g, @Nonnull Term t, boolean antecedent)
t
- Term to add to teh sequentantecedent
- whether to add teh term to antecedentpublic Node applyChangeFormula(@Nonnull Goal g, @Nonnull PosInOccurrence pio, @Nonnull Term term, @Nonnull Term newTerm)
public void soundHide(Goal g, PosInOccurrence pio, Term term)
Copyright © 2003-2019 The KeY-Project.