public abstract class AbstractPropositionalExpansionMacro extends StrategyProofMacro
getAdmittedRuleNames()
.
This is very helpful to perform many "andLeft", "impRight" or even "andRight"
steps at a time.Modifier and Type | Class and Description |
---|---|
private class |
AbstractPropositionalExpansionMacro.PropExpansionStrategy
This strategy accepts all rule apps for which the rule name is in the
admitted set and rejects everything else.
|
ProofMacro.ProgressBarListener
Constructor and Description |
---|
AbstractPropositionalExpansionMacro() |
Modifier and Type | Method and Description |
---|---|
protected abstract boolean |
allowOSS()
Whether this macro includes One Step Simplification.
|
protected static Set<String> |
asSet(String[] strings) |
protected Strategy |
createStrategy(Proof proof,
PosInOccurrence posInOcc) |
protected abstract Set<String> |
getAdmittedRuleNames()
Gets the set of admitted rule names.
|
String |
getCategory()
Gets the category of this macro.
|
protected boolean |
ruleApplicationInContextAllowed(RuleApp ruleApp,
PosInOccurrence pio,
Goal goal)
Checks whether the application of the passed rule is ok in the given
context.
|
applyTo, canApplyTo, doPostProcessing
applyTo, canApplyTo, getMaxSteps, getScriptCommandName
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
getDescription, getName
public String getCategory()
ProofMacro
null
if no submenu is to be created.null
protected abstract Set<String> getAdmittedRuleNames()
null
setprotected abstract boolean allowOSS()
protected Strategy createStrategy(Proof proof, PosInOccurrence posInOcc)
createStrategy
in class StrategyProofMacro
protected boolean ruleApplicationInContextAllowed(RuleApp ruleApp, PosInOccurrence pio, Goal goal)
ruleApp
- rule to be appliedpio
- contextgoal
- context