Class Disjunction

java.lang.Object

org.tweetyproject.logics.pl.syntax.PlFormula

org.tweetyproject.logics.pl.syntax.AssociativePlFormula

org.tweetyproject.logics.pl.syntax.Disjunction

All Implemented Interfaces:

Iterable<PlFormula>, Collection<PlFormula>, List<PlFormula>, SequencedCollection<PlFormula>, Formula, AssociativeFormulaSupport.AssociativeSupportBridge, AssociativeFormula<PlFormula>, ClassicalFormula, Conjunctable, Disjunctable, Invertable, ProbabilityAware, SimpleLogicalFormula

public class Disjunction
extends AssociativePlFormula

This class represents a disjunction in propositional logic.

Author:

Matthias Thimm, Tim Janus

Constructor Summary

Constructors

Constructor	Description
Disjunction()	Creates a new (empty) disjunction.
Disjunction(Collection<? extends PlFormula> formulas)	Creates a new disjunction with the given inner formulas.
Disjunction(PlFormula... formulas)	constructor
Disjunction(PlFormula first, PlFormula second)	Creates a new disjunction with the two given formulae

Method Summary

Modifier and Type	Method	Description
PlFormula	clone()	Creates a deep copy of this formula
PlFormula	collapseAssociativeFormulas()	This method collapses all associative operations appearing in this term, e.g.
Disjunction	createEmptyFormula()
String	getEmptySymbol()
Set<PossibleWorld>	getModels(PlSignature sig)	Returns the set of models of this formula wrt.
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 org.tweetyproject.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 org.tweetyproject.logics.pl.syntax.PlFormula

combineWithAnd, combineWithOr, complement, getModels, getPredicateCls, getPrimeImplicants, getUniformProbability, isConjunctiveClause, isLiteral, resolvableWith, resolveWith, toBlakeCanonicalForm, toDnf

Methods inherited from class java.lang.Object

getClass, notify, notifyAll, wait, wait, wait

Methods inherited from interface java.util.Collection

parallelStream, removeIf, stream, toArray

Methods inherited from interface java.lang.Iterable

forEach

Methods inherited from interface java.util.List

addFirst, addLast, getFirst, getLast, removeFirst, removeLast, replaceAll, reversed, sort, spliterator

Methods inherited from interface org.tweetyproject.logics.commons.syntax.interfaces.SimpleLogicalFormula

getPredicateCls, isLiteral

Constructor Details

Disjunction

public Disjunction(Collection<? extends PlFormula> formulas)

Creates a new disjunction with the given inner formulas.

Parameters:

formulas - a collection of formulas.

Disjunction

public Disjunction(PlFormula... formulas)

constructor

Parameters:

formulas - formulas

Disjunction

public Disjunction()

Creates a new (empty) disjunction.

Disjunction

public Disjunction(PlFormula first,
 PlFormula second)

Creates a new disjunction 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 PlFormula 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 Disjunction 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 Set<PossibleWorld> 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.

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.

Overrides:

isClause in class PlFormula

Returns:

"true" iff this formula is a 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.