public interface _AbstractFormula
Represents a formula during proof-search. The engine needs very little
information about the formulas on which the proof-search works. Indeed,
formulas are explicitly used only by the implementation of the rules of the
calculus (i.e., implementations of _RegularRule
and
_BranchExistsRule
) and by the implementation of goals (
_AbstractGoal
). The engine only uses the methods shortName()
and format()
when it works in verbose mode to print information on
the proof-search. The short name should specify some essential information
about the formula; e.g., in the case of a sequent calculus implementation, it
should be something like left-AND
, to mean that this is a
formula with AND as main connective belonging to the left hand-side of the
sequent.
Modifier and Type | Method and Description |
---|---|
java.lang.String |
format()
Returns the string representation of the formula
|
java.lang.String |
shortName()
Returns the short name of the formula.
|
java.lang.String format()
java.lang.String shortName()