public class Conjunction extends AssociativePropositionalFormula
support| Constructor and Description | 
|---|
Conjunction()
Creates a new (empty) conjunction. 
 | 
Conjunction(java.util.Collection<? extends PropositionalFormula> formulas)
Creates a new conjunction with the given inner formulas. 
 | 
Conjunction(PropositionalFormula first,
           PropositionalFormula 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 
 | 
PropositionalFormula | 
collapseAssociativeFormulas()
This method collapses all associative operations appearing
 in this term, e.g. 
 | 
Conjunction | 
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 | 
isConjunctiveClause()
Checks whether this formula is a conjunctive 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, toStringcombineWithAnd, combineWithOr, complement, getModels, getPredicateCls, getPrimeImplicants, getUniformProbability, isLiteral, resolvableWith, resolveWith, toBlakeCanonicalForm, toDnffinalize, getClass, notify, notifyAll, wait, wait, waitgetPredicateCls, isLiteralpublic Conjunction(java.util.Collection<? extends PropositionalFormula> formulas)
formulas - a collection of formulas.public Conjunction()
public Conjunction(PropositionalFormula first, PropositionalFormula second)
first - a propositional formula.second - a propositional formula.public PropositionalFormula collapseAssociativeFormulas()
PropositionalFormulacollapseAssociativeFormulas in class PropositionalFormulapublic PropositionalFormula toNnf()
PropositionalFormulatoNnf in class PropositionalFormulapublic Conjunction clone()
SimpleLogicalFormulaclone in interface SimpleLogicalFormulaclone in class PropositionalFormulapublic Conjunction createEmptyFormula()
public java.lang.String getOperatorSymbol()
public java.lang.String getEmptySymbol()
public Conjunction toCnf()
PropositionalFormulatoCnf in class PropositionalFormulapublic PropositionalFormula trim()
PropositionalFormulatrim in class PropositionalFormulapublic java.util.Set<PossibleWorld> getModels(PropositionalSignature sig)
PropositionalFormulagetModels in class PropositionalFormulasig - some propositional signaturepublic boolean isConjunctiveClause()
PropositionalFormulaisConjunctiveClause in class PropositionalFormulapublic PropositionalFormula replace(Proposition p, PropositionalFormula f, int i)
PropositionalFormulareplace in class PropositionalFormulap - some propositionf - some formulai - the index of the proposition