Package net.sf.tweety.logics.pl.syntax
Class ExclusiveDisjunction
- java.lang.Object
-
- net.sf.tweety.logics.pl.syntax.PlFormula
-
- net.sf.tweety.logics.pl.syntax.AssociativePlFormula
-
- net.sf.tweety.logics.pl.syntax.ExclusiveDisjunction
-
- All Implemented Interfaces:
java.lang.Iterable<PlFormula>
,java.util.Collection<PlFormula>
,java.util.List<PlFormula>
,Formula
,AssociativeFormulaSupport.AssociativeSupportBridge
,AssociativeFormula<PlFormula>
,ClassicalFormula
,Conjunctable
,Disjunctable
,Invertable
,ProbabilityAware
,SimpleLogicalFormula
public class ExclusiveDisjunction extends AssociativePlFormula
This class represents an exclusive disjunction (XOR) in propositional logic.- Author:
- Anna Gessler, Matthias Thimm
-
-
Constructor Summary
Constructors Constructor Description ExclusiveDisjunction()
Creates a new (empty) exclusive disjunction.ExclusiveDisjunction(java.util.Collection<? extends PlFormula> formulas)
Creates a new XOR formula with the given inner formulas.ExclusiveDisjunction(PlFormula first, PlFormula second)
Creates a new exclusive disjunction with the two given formulae
-
Method Summary
Modifier and Type Method Description PlFormula
clone()
Creates a deep copy of this formulaPlFormula
collapseAssociativeFormulas()
This method collapses all associative operations appearing in this term, e.g.ExclusiveDisjunction
createEmptyFormula()
java.lang.String
getEmptySymbol()
java.util.Set<PossibleWorld>
getModels(PlSignature 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.PlFormula
replace(Proposition p, PlFormula 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).PlFormula
toNnf()
This method returns this formula in negation normal form (NNF).PlFormula
trim()
Removes duplicates (identical formulas) from conjunctions and disjunctions and removes duplicate negations.-
Methods inherited from class net.sf.tweety.logics.pl.syntax.AssociativePlFormula
add, 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
-
Methods inherited from class net.sf.tweety.logics.pl.syntax.PlFormula
combineWithAnd, combineWithOr, complement, getModels, getPredicateCls, getPrimeImplicants, getUniformProbability, isConjunctiveClause, isLiteral, resolvableWith, resolveWith, toBlakeCanonicalForm, toDnf
-
Methods inherited from interface net.sf.tweety.logics.commons.syntax.interfaces.SimpleLogicalFormula
getPredicateCls, isLiteral
-
-
-
-
Constructor Detail
-
ExclusiveDisjunction
public ExclusiveDisjunction(java.util.Collection<? extends PlFormula> formulas)
Creates a new XOR formula with the given inner formulas.- Parameters:
formulas
- a collection of formulas.
-
ExclusiveDisjunction
public ExclusiveDisjunction()
Creates a new (empty) exclusive disjunction.
-
-
Method Detail
-
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 classPlFormula
- 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.
-
clone
public PlFormula clone()
Description copied from interface:SimpleLogicalFormula
Creates a deep copy of this formula- Specified by:
clone
in interfaceSimpleLogicalFormula
- Specified by:
clone
in classPlFormula
- Returns:
- the cloned formula
-
createEmptyFormula
public ExclusiveDisjunction createEmptyFormula()
- Returns:
- an empty version of the AssociativeFormula
-
getOperatorSymbol
public java.lang.String getOperatorSymbol()
- Returns:
- A String representing the operator which connects two items of the associative formula.
-
getEmptySymbol
public java.lang.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.
-
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.
-
getModels
public java.util.Set<PossibleWorld> getModels(PlSignature sig)
Description copied from class:PlFormula
Returns the set of models of this formula wrt. the given signature.
-
isClause
public boolean isClause()
Description copied from class:PlFormula
Checks whether this formula is a clause, i.e. whether it is a disjunction of literals.
-
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.
-
-