Package org.tweetyproject.logics.pl.syntax

Class SpecialFormula

java.lang.Object

org.tweetyproject.logics.pl.syntax.PlFormula

org.tweetyproject.logics.pl.syntax.SpecialFormula

All Implemented Interfaces:

Formula, ClassicalFormula, Conjunctable, Disjunctable, Invertable, ProbabilityAware, SimpleLogicalFormula

Direct Known Subclasses:

Contradiction, Tautology

public abstract class SpecialFormula
extends PlFormula

This class captures the common functionalities of the special formulas tautology and contradiction.

Author:

Matthias Thimm

Constructor Summary

Constructors

Constructor	Description
SpecialFormula()	Default Constructor

Method Summary

Modifier and Type	Method	Description
PlFormula	collapseAssociativeFormulas()	This method collapses all associative operations appearing in this term, e.g.
Set<Proposition>	getAtoms()	Processes the set of all atoms which appear in this formula
Set<PlFormula>	getLiterals()	Returns all literals, i.e.
Set<PlPredicate>	getPredicates()	Processes the set of all predicates which appear in this formula
int	numberOfOccurrences(Proposition p)	Returns the number of occurrences of the given proposition within this formula
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.PlFormula

clone, combineWithAnd, combineWithOr, complement, equals, getModels, getModels, getPredicateCls, getPrimeImplicants, getSignature, getUniformProbability, hashCode, isClause, isConjunctiveClause, isLiteral, resolvableWith, resolveWith, toBlakeCanonicalForm, toDnf

Methods inherited from class java.lang.Object

getClass, notify, notifyAll, toString, wait, wait, wait

Constructor Details

SpecialFormula

public SpecialFormula()

Default Constructor

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.

getPredicates

public Set<PlPredicate> getPredicates()

Description copied from interface: SimpleLogicalFormula

Processes the set of all predicates which appear in this formula

Specified by:

getPredicates in interface SimpleLogicalFormula

Specified by:

getPredicates in class PlFormula

Returns:

all predicates that appear in this 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.

getAtoms

public Set<Proposition> getAtoms()

Description copied from interface: SimpleLogicalFormula

Processes the set of all atoms which appear in this formula

Specified by:

getAtoms in interface SimpleLogicalFormula

Specified by:

getAtoms in class PlFormula

Returns:

The set of all atoms

getLiterals

public Set<PlFormula> getLiterals()

Description copied from class: PlFormula

Returns all literals, i.e. all formulas of the form "a" or "!a" where "a" is a proposition, that appear in this formula.

Specified by:

getLiterals in class PlFormula

Returns:

all literals appearing in this formula.

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.

numberOfOccurrences

public int numberOfOccurrences(Proposition p)

Description copied from class: PlFormula

Returns the number of occurrences of the given proposition within this formula

Specified by:

numberOfOccurrences in class PlFormula

Parameters:

p - some proposition

Returns:

the number of occurrences of the given proposition within this formula

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.

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.