public abstract class ModalFormula extends RelationalFormula
Modifier and Type | Field and Description |
---|---|
private RelationalFormula |
formula
The inner formula of this modal formula
|
Constructor and Description |
---|
ModalFormula(RelationalFormula formula) |
Modifier and Type | Method and Description |
---|---|
Conjunction |
combineWithAnd(Conjuctable f)
Returns a conjunction of this and the given formula.
|
Disjunction |
combineWithOr(Disjunctable f) |
RelationalFormula |
complement() |
boolean |
containsQuantifier()
Checks whether this formula contains any quantification.
|
boolean |
equals(java.lang.Object obj) |
java.util.Set<FOLAtom> |
getAtoms()
Processes the set of all atoms which appear in this formula
|
RelationalFormula |
getFormula()
Returns the inner formula of this modal formula.
|
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<Variable> |
getQuantifierVariables() |
FolSignature |
getSignature()
Returns the signature of the language of 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() |
Probability |
getUniformProbability() |
int |
hashCode() |
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 |
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.
|
RelationalFormula |
substitute(Term<?> v,
Term<?> t)
Substitutes all occurrences of term "v" in this formula
by term "t" and returns the new formula.
|
allGroundInstances, allSubstitutions, clone, containsTermsOfType, exchange, getPredicateCls, getSatisfactionRatio, isGround, isWellFormed, substitute, toString
private RelationalFormula formula
public ModalFormula(RelationalFormula formula)
public FolSignature getSignature()
Formula
getSignature
in interface Formula
getSignature
in class RelationalFormula
public Probability getUniformProbability()
getUniformProbability
in interface ProbabilityAware
getUniformProbability
in class RelationalFormula
public RelationalFormula getFormula()
getFormula
in interface QuantifiedFormula
getFormula
in class RelationalFormula
public java.util.Set<? extends Predicate> getPredicates()
SimpleLogicalFormula
public java.util.Set<Functor> getFunctors()
getFunctors
in class RelationalFormula
public java.util.Set<FOLAtom> getAtoms()
SimpleLogicalFormula
getAtoms
in interface SimpleLogicalFormula
getAtoms
in class RelationalFormula
public boolean containsQuantifier()
QuantifiedFormula
public boolean isClosed()
QuantifiedFormula
public boolean isClosed(java.util.Set<Variable> boundVariables)
QuantifiedFormula
boundVariables
- the variables assumed to be bound.public java.util.Set<Variable> getUnboundVariables()
public boolean isWellBound()
QuantifiedFormula
public boolean isWellBound(java.util.Set<Variable> boundVariables)
QuantifiedFormula
boundVariables
- the variables assumed to be bound.public Conjunction combineWithAnd(Conjuctable f)
Conjuctable
combineWithAnd
in interface Conjuctable
combineWithAnd
in class RelationalFormula
f
- a formula to be combined with AND and this.public Disjunction combineWithOr(Disjunctable f)
combineWithOr
in interface Disjunctable
combineWithOr
in class RelationalFormula
f
- a formula to be combined with OR and this.public RelationalFormula complement()
complement
in interface Invertable
complement
in class RelationalFormula
public boolean isLiteral()
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<Variable> getQuantifierVariables()
public RelationalFormula substitute(Term<?> v, Term<?> t) throws java.lang.IllegalArgumentException
RelationalFormula
substitute
in interface ComplexLogicalFormula
substitute
in class RelationalFormula
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 int hashCode()
hashCode
in interface SimpleLogicalFormula
hashCode
in class java.lang.Object
public boolean equals(java.lang.Object obj)
equals
in interface SimpleLogicalFormula
equals
in class java.lang.Object