public class Disjunction extends AssociativePropositionalFormula
support
Constructor and Description |
---|
Disjunction()
Creates a new (empty) disjunction.
|
Disjunction(java.util.Collection<? extends PropositionalFormula> formulas)
Creates a new disjunction with the given inner formulas.
|
Disjunction(PropositionalFormula first,
PropositionalFormula second)
Creates a new disjunction with the two given formulae
|
Modifier and Type | Method and Description |
---|---|
PropositionalFormula |
clone()
Creates a deep copy of this formula
|
PropositionalFormula |
collapseAssociativeFormulas()
This method collapses all associative operations appearing
in this term, e.g.
|
Disjunction |
createEmptyFormula() |
java.lang.String |
getEmptySymbol() |
java.util.Set<PossibleWorld> |
getModels(PropositionalSignature sig)
Returns the set of models of this formula wrt.
|
java.lang.String |
getOperatorSymbol() |
boolean |
isClause()
Checks whether this formula is a clause,
i.e.
|
PropositionalFormula |
replace(Proposition p,
PropositionalFormula f,
int i)
Replaces the ith instance of the proposition p by f.
|
Conjunction |
toCnf()
This method returns this formula in conjunctive normal form (CNF).
|
PropositionalFormula |
toNnf()
This method returns this formula in negation normal form (NNF).
|
PropositionalFormula |
trim()
Removes duplicates (identical formulas) from conjunctions and disjunctions and
duplicate negations.
|
add, add, addAll, addAll, clear, contains, containsAll, createEmptySignature, equals, get, getAtoms, getFormulas, getFormulas, getLiterals, getPredicates, getSignature, hashCode, indexOf, isEmpty, iterator, lastIndexOf, listIterator, listIterator, numberOfOccurrences, remove, remove, removeAll, retainAll, set, size, subList, toArray, toArray, toString
combineWithAnd, combineWithOr, complement, getModels, getPredicateCls, getPrimeImplicants, getUniformProbability, isConjunctiveClause, isLiteral, resolvableWith, resolveWith, toBlakeCanonicalForm, toDnf
finalize, getClass, notify, notifyAll, wait, wait, wait
getPredicateCls, isLiteral
public Disjunction(java.util.Collection<? extends PropositionalFormula> formulas)
formulas
- a collection of formulas.public Disjunction()
public Disjunction(PropositionalFormula first, PropositionalFormula second)
first
- a propositional formula.second
- a propositional formula.public PropositionalFormula collapseAssociativeFormulas()
PropositionalFormula
collapseAssociativeFormulas
in class PropositionalFormula
public PropositionalFormula toNnf()
PropositionalFormula
toNnf
in class PropositionalFormula
public PropositionalFormula clone()
SimpleLogicalFormula
clone
in interface SimpleLogicalFormula
clone
in class PropositionalFormula
public Disjunction createEmptyFormula()
public java.lang.String getOperatorSymbol()
public java.lang.String getEmptySymbol()
public Conjunction toCnf()
PropositionalFormula
toCnf
in class PropositionalFormula
public PropositionalFormula trim()
PropositionalFormula
trim
in class PropositionalFormula
public java.util.Set<PossibleWorld> getModels(PropositionalSignature sig)
PropositionalFormula
getModels
in class PropositionalFormula
sig
- some propositional signaturepublic boolean isClause()
PropositionalFormula
isClause
in class PropositionalFormula
public PropositionalFormula replace(Proposition p, PropositionalFormula f, int i)
PropositionalFormula
replace
in class PropositionalFormula
p
- some propositionf
- some formulai
- the index of the proposition