public class Implication extends FolFormula
Modifier and Type | Field and Description |
---|---|
private Pair<RelationalFormula,RelationalFormula> |
formulas
The pair of formulas that are part of the implication.
|
Constructor and Description |
---|
Implication(Pair<RelationalFormula,RelationalFormula> formulas)
Creates a new implication with the given pair of formulas
|
Implication(RelationalFormula a,
RelationalFormula b)
Creates a new implication a=>b with the two given formulas
|
Modifier and Type | Method and Description |
---|---|
FolFormula |
clone()
Creates a deep copy of this formula
|
RelationalFormula |
collapseAssociativeFormulas()
This method collapses all associative operations appearing
in this term, e.g.
|
boolean |
containsQuantifier()
Checks whether this formula contains any quantification.
|
java.util.Set<? extends Atom> |
getAtoms()
Processes the set of all atoms which appear in this formula
|
Pair<RelationalFormula,RelationalFormula> |
getFormulas()
Returns the formulas of the implication.
|
java.util.Set<Functor> |
getFunctors() |
java.util.Set<? extends Predicate> |
getPredicates()
Processes the set of all predicates which appear in this
formula
|
java.util.Set<Term<?>> |
getTerms() |
<C extends Term<?>> |
getTerms(java.lang.Class<C> cls)
Processes the set containing all terms of type C.
|
java.util.Set<Variable> |
getUnboundVariables() |
boolean |
isClosed()
Checks whether this formula is closed, i.e.
|
boolean |
isClosed(java.util.Set<Variable> boundVariables)
Checks whether this formula is closed, i.e.
|
boolean |
isDnf()
Checks whether this formula is in disjunctive normal form.
|
boolean |
isLiteral() |
boolean |
isWellBound()
Checks whether this formula is well-bound, i.e.
|
boolean |
isWellBound(java.util.Set<Variable> boundVariables)
Checks whether this formula is well-bound, i.e.
|
void |
setFormulas(Pair<RelationalFormula,RelationalFormula> formulas)
Sets the formulas of the implication.
|
FolFormula |
substitute(Term<?> v,
Term<?> t)
Substitutes all occurrences of term "v" in this formula
by term "t" and returns the new formula.
|
FolFormula |
toNnf()
Makes the negation normal form of this formula.
|
java.lang.String |
toString() |
combineWithAnd, combineWithOr, complement, getQuantifierVariables, getSignature, getUniformProbability, toDnf
allGroundInstances, allSubstitutions, containsTermsOfType, exchange, getFormula, getPredicateCls, getSatisfactionRatio, isGround, isWellFormed, substitute
equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
equals, hashCode
private Pair<RelationalFormula,RelationalFormula> formulas
public Implication(RelationalFormula a, RelationalFormula b)
a
- a relational formula.b
- a relational formula.public Implication(Pair<RelationalFormula,RelationalFormula> formulas)
formulas
- a pair of formulaspublic Pair<RelationalFormula,RelationalFormula> getFormulas()
public void setFormulas(Pair<RelationalFormula,RelationalFormula> formulas)
the
- formulaspublic java.util.Set<? extends Predicate> getPredicates()
SimpleLogicalFormula
public boolean isLiteral()
public java.util.Set<Variable> getUnboundVariables()
public boolean containsQuantifier()
QuantifiedFormula
public boolean isWellBound()
QuantifiedFormula
public boolean isWellBound(java.util.Set<Variable> boundVariables)
QuantifiedFormula
boundVariables
- the variables assumed to be bound.public boolean isClosed()
QuantifiedFormula
public boolean isClosed(java.util.Set<Variable> boundVariables)
QuantifiedFormula
boundVariables
- the variables assumed to be bound.public java.util.Set<Term<?>> getTerms()
public <C extends Term<?>> java.util.Set<C> getTerms(java.lang.Class<C> cls)
LogicStructure
cls
- The Class structure containing type information about the
searched termpublic FolFormula toNnf()
FolFormula
toNnf
in class FolFormula
public RelationalFormula collapseAssociativeFormulas()
FolFormula
collapseAssociativeFormulas
in class FolFormula
public boolean isDnf()
FolFormula
isDnf
in class FolFormula
public FolFormula substitute(Term<?> v, Term<?> t) throws java.lang.IllegalArgumentException
RelationalFormula
substitute
in interface ComplexLogicalFormula
substitute
in class FolFormula
v
- the term to be substituted.t
- the term to substitute.java.lang.IllegalArgumentException
- if "v" and "t" are of different sorts
(NOTE: this exception is only thrown when "v" actually appears in this
formula).public FolFormula clone()
SimpleLogicalFormula
clone
in interface ComplexLogicalFormula
clone
in interface SimpleLogicalFormula
clone
in class FolFormula
public java.util.Set<? extends Atom> getAtoms()
SimpleLogicalFormula
getAtoms
in interface SimpleLogicalFormula
getAtoms
in class RelationalFormula
public java.util.Set<Functor> getFunctors()
getFunctors
in class RelationalFormula
public java.lang.String toString()
toString
in class RelationalFormula