public interface _SingleSuccedentSequent extends _AbstractGoal
S ==> H
where
S
is a sets of propositional formulas and H
is a
propositional formula.Modifier and Type | Method and Description |
---|---|
void |
addLeft(Formula wff)
Add the specified formula to the left hand side of this sequent.
|
void |
addRight(Formula wff)
This method add the specified formula in the right hand side of this
sequent.
|
_SingleSuccedentSequent |
clone()
Returns a fresh copy of this sequent.
|
boolean |
containsLeft(Formula wff)
Returns
true if this sequent contains the specified formula in
the left hand side and false otherwise. |
java.util.Collection<Formula> |
getAllLeftFormulas()
Returns the set containg all the formulas in the left hand side of this
sequent or
null if the left hand side of this sequent is
empty. |
java.util.Collection<Formula> |
getAllLeftFormulas(FormulaType formulaType)
Returns the collection of all the formulas in the left hand side of this
sequent with the specified type or
null if the left hand side
of this sequent does not contain any formula of the specified type. |
Formula |
getLeft()
Returns a formula from the left hand side of the sequent or
null if le theft hand side is empty. |
Formula |
getLeft(FormulaType formulaType)
Returns a formula of the specified type contained in the left hand side of
the sequent or
null if no formula of the specified type occurs
in this sequent. |
Formula |
getRight()
Returns the formula in the right hand side of this sequent or
null if the right hand side of this sequent is empty. |
Formula |
getRightFormulaOfType(FormulaType formulaType)
Returns the formula in the right hand side of this sequent if the formula
has the specified type or
null if the formula in the right
hand side does not have the specified type. |
boolean |
isIdentityAxiom()
Returns
true iff this is an identity axiom, that is a sequent
of the kind S,H ==> H . |
boolean |
removeLeft(Formula wff)
Removes the specified formula from the left hand side of this sequent, if
it is present.
|
boolean |
removeRight()
Removes the right formula form this sequent.
|
format
void addLeft(Formula wff)
wff
- the formula to add.void addRight(Formula wff)
wff
- the formula to add in the right hand side of the sequent._SingleSuccedentSequent clone()
clone
in interface _AbstractGoal
boolean containsLeft(Formula wff)
true
if this sequent contains the specified formula in
the left hand side and false otherwise.wff
- the formula to searchtrue
if the right hand side of the sequent contains
the specifiedjava.util.Collection<Formula> getAllLeftFormulas()
null
if the left hand side of this sequent is
empty.null
.java.util.Collection<Formula> getAllLeftFormulas(FormulaType formulaType)
null
if the left hand side
of this sequent does not contain any formula of the specified type.formulaType
- the type of the formulas.null
if the left hand side of the sequent does not contain any
formula of the sepcified type.Formula getRight()
null
if the right hand side of this sequent is empty.null
.Formula getLeft(FormulaType formulaType)
null
if no formula of the specified type occurs
in this sequent.formulaType
- the type of the formula to be returnednull
.Formula getLeft()
null
if le theft hand side is empty.null
.Formula getRightFormulaOfType(FormulaType formulaType)
null
if the formula in the right
hand side does not have the specified type.formulaType
- the type of the formula to be returnednull
if the type of the formula in the right hand
side is different from the specified type.boolean isIdentityAxiom()
true
iff this is an identity axiom, that is a sequent
of the kind S,H ==> H
.true
iff this is an identity axiom.boolean removeLeft(Formula wff)
wff
- the formula to remove.true
if this sequent contained the specified element.boolean removeRight()
true
if this sequent contained a formula in the
right-hand side.