# Class Conjunction

All Implemented Interfaces:
Iterable<PlFormula>, Collection<PlFormula>, List<PlFormula>, Formula, AssociativeFormulaSupport.AssociativeSupportBridge, AssociativeFormula<PlFormula>, ClassicalFormula, Conjunctable, Disjunctable, Invertable, ProbabilityAware, SimpleLogicalFormula

public class Conjunction extends AssociativePlFormula
This class represents a conjunction in propositional logic.
Author:
Matthias Thimm, Tim Janus
• ## Constructor Details

• ### Conjunction

public Conjunction(Collection<? extends PlFormula> formulas)
Creates a new conjunction with the given inner formulas.
Parameters:
formulas - a collection of formulas.
• ### Conjunction

public Conjunction()
Creates a new (empty) conjunction.
• ### Conjunction

public Conjunction(PlFormula first, PlFormula second)
Creates a new conjunction with the two given formulae
Parameters:
first - a propositional formula.
second - a propositional formula.
• ## Method Details

• ### collapseAssociativeFormulas

public PlFormula collapseAssociativeFormulas()
Description copied from class: PlFormula
This method collapses all associative operations appearing in this term, e.g. every a||(b||c) becomes a||b||c.
Specified by:
collapseAssociativeFormulas in class PlFormula
Returns:
the collapsed formula.
• ### toNnf

public PlFormula toNnf()
Description copied from class: PlFormula
This method returns this formula in negation normal form (NNF). A formula is in NNF iff negations occur only directly in front of a proposition.
Specified by:
toNnf in class PlFormula
Returns:
the formula in NNF.
• ### clone

public Conjunction clone()
Description copied from interface: SimpleLogicalFormula
Creates a deep copy of this formula
Specified by:
clone in interface SimpleLogicalFormula
Specified by:
clone in class PlFormula
Returns:
the cloned formula
• ### createEmptyFormula

public Conjunction createEmptyFormula()
Returns:
an empty version of the AssociativeFormula
• ### getOperatorSymbol

public String getOperatorSymbol()
Returns:
A String representing the operator which connects two items of the associative formula.
• ### getEmptySymbol

public String getEmptySymbol()
Returns:
A String representing an empty version of the Associative Formula implementation
• ### toCnf

public Conjunction toCnf()
Description copied from class: PlFormula
This method returns this formula in conjunctive normal form (CNF). A formula is in CNF iff it is a conjunction of disjunctions and in NNF. The CNF generated by this method is not necessarily minimal.
Specified by:
toCnf in class PlFormula
Returns:
the formula in CNF.
• ### trim

public PlFormula trim()
Description copied from class: PlFormula
Removes duplicates (identical formulas) from conjunctions and disjunctions and removes duplicate negations. Simplifies equivalences and implications with equivalent formulas (A=>A, A<=>A) to tautologies.
Specified by:
trim in class PlFormula
Returns:
an equivalent formula without duplicates.
• ### getModels

public  getModels(PlSignature sig)
Description copied from class: PlFormula
Returns the set of models of this formula wrt. the given signature.
Specified by:
getModels in class PlFormula
Parameters:
sig - some propositional signature
Returns:
the set of models of this formula wrt. the given signature.
• ### isConjunctiveClause

public boolean isConjunctiveClause()
Description copied from class: PlFormula
Checks whether this formula is a conjunctive clause, i.e. whether it is a conjunction of literals.
Overrides:
isConjunctiveClause in class PlFormula
Returns:
"true" iff this formula is a conjunctive clause.
• ### replace

public PlFormula replace(Proposition p, PlFormula f, int i)
Description copied from class: PlFormula
Replaces the ith instance of the proposition p by f.
Specified by:
replace in class PlFormula
Parameters:
p - some proposition
f - some formula
i - the index of the proposition
Returns:
a new formula with the ith instance of the proposition p replaced by f.