public abstract class SpecialFormula extends FolFormula
Constructor and Description |
---|
SpecialFormula() |
Modifier and Type | Method and Description |
---|---|
FolFormula |
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<FOLAtom> |
getAtoms()
Processes the set of all atoms which appear in this formula
|
java.util.Set<Conjunction> |
getConjunctions() |
java.util.Set<Disjunction> |
getDisjunctions() |
java.util.Set<Functor> |
getFunctors() |
java.util.Set<Predicate> |
getPredicates()
Processes the set of all predicates which appear in this
formula
|
java.util.Set<QuantifiedFormula> |
getQuantifiedFormulas() |
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.
|
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.
|
clone, combineWithAnd, combineWithOr, complement, getQuantifierVariables, getUniformProbability, toDnf
allGroundInstances, allSubstitutions, containsTermsOfType, exchange, getFormula, getPredicateCls, getSatisfactionRatio, getSignature, isGround, isWellFormed, substitute, toString
equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
equals, hashCode
public boolean containsQuantifier()
QuantifiedFormula
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 java.util.Set<FOLAtom> getAtoms()
SimpleLogicalFormula
getAtoms
in interface SimpleLogicalFormula
getAtoms
in class RelationalFormula
public java.util.Set<Predicate> getPredicates()
SimpleLogicalFormula
public boolean isClosed()
QuantifiedFormula
public boolean isClosed(java.util.Set<Variable> boundVariables)
QuantifiedFormula
boundVariables
- the variables assumed to be bound.public boolean isWellBound()
QuantifiedFormula
public boolean isWellBound(java.util.Set<Variable> boundVariables)
QuantifiedFormula
boundVariables
- the variables assumed to be bound.public boolean isLiteral()
public FolFormula substitute(Term<?> v, Term<?> t)
RelationalFormula
substitute
in interface ComplexLogicalFormula
substitute
in class FolFormula
v
- the term to be substituted.t
- the term to substitute.public java.util.Set<Variable> getUnboundVariables()
public java.util.Set<Functor> getFunctors()
getFunctors
in class RelationalFormula
public java.util.Set<QuantifiedFormula> getQuantifiedFormulas()
public java.util.Set<Disjunction> getDisjunctions()
public java.util.Set<Conjunction> getConjunctions()
public boolean isDnf()
FolFormula
isDnf
in class FolFormula
public FolFormula toNnf()
FolFormula
toNnf
in class FolFormula
public FolFormula collapseAssociativeFormulas()
FolFormula
collapseAssociativeFormulas
in class FolFormula