public class Conjunction extends AssociativeFOLFormula
support
Constructor and Description |
---|
Conjunction()
Creates a new (empty) conjunction.
|
Conjunction(java.util.Collection<? extends RelationalFormula> formulas)
Creates a new conjunction with the given inner formulas.
|
Conjunction(RelationalFormula first,
RelationalFormula second)
Creates a new conjunction with the two given formulae
|
Modifier and Type | Method and Description |
---|---|
Conjunction |
clone()
Creates a deep copy of this formula
|
RelationalFormula |
collapseAssociativeFormulas()
This method collapses all associative operations appearing
in this term, e.g.
|
Conjunction |
createEmptyFormula() |
java.lang.String |
getEmptySymbol() |
java.lang.String |
getOperatorSymbol() |
boolean |
isDnf()
Checks whether this formula is in disjunctive normal form.
|
Conjunction |
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.
|
add, add, addAll, addAll, clear, contains, containsAll, containsQuantifier, createEmptySignature, equals, get, getAtoms, getFormulas, getFormulas, getFunctors, getPredicates, getQuantifierVariables, getTerms, getTerms, getUnboundVariables, hashCode, indexOf, isClosed, isClosed, isEmpty, isLiteral, isWellBound, isWellBound, iterator, lastIndexOf, listIterator, listIterator, remove, remove, removeAll, retainAll, set, size, subList, substitute, toArray, toArray, toString
combineWithAnd, combineWithOr, complement, getSignature, getUniformProbability, toDnf
allGroundInstances, allSubstitutions, containsTermsOfType, exchange, getFormula, getPredicateCls, getSatisfactionRatio, isGround, isWellFormed
finalize, getClass, notify, notifyAll, wait, wait, wait
getPredicateCls
getSignature
public Conjunction(java.util.Collection<? extends RelationalFormula> formulas)
formulas
- a collection of formulas.public Conjunction()
public Conjunction(RelationalFormula first, RelationalFormula second)
first
- a relational formula.second
- a relational formula.public boolean isDnf()
FolFormula
isDnf
in class FolFormula
public Conjunction substitute(Term<?> v, Term<?> t) throws java.lang.IllegalArgumentException
RelationalFormula
substitute
in interface ComplexLogicalFormula
substitute
in class AssociativeFOLFormula
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 toNnf()
FolFormula
toNnf
in class FolFormula
public RelationalFormula collapseAssociativeFormulas()
FolFormula
collapseAssociativeFormulas
in class FolFormula
public Conjunction clone()
SimpleLogicalFormula
clone
in interface ComplexLogicalFormula
clone
in interface SimpleLogicalFormula
clone
in class FolFormula
public Conjunction createEmptyFormula()
public java.lang.String getOperatorSymbol()
public java.lang.String getEmptySymbol()