Package org.tweetyproject.logics.pl.syntax

Class PlFormula

java.lang.Object

org.tweetyproject.logics.pl.syntax.PlFormula

All Implemented Interfaces:

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

Direct Known Subclasses:

AssociativePlFormula, Equivalence, ExistsQuantifiedFormula, ForallQuantifiedFormula, Implication, Indecision, Negation, Proposition, SpecialFormula, WeakNegation

public abstract class PlFormula
extends Object
implements ClassicalFormula

This class represents the common ancestor for propositional formulae.

Author:

Matthias Thimm, Tim Janus

Constructor Summary

Constructors

Constructor	Description
PlFormula()	Default Constructor

Method Summary

Modifier and Type	Method	Description
abstract PlFormula	clone()	Creates a deep copy of this formula
abstract PlFormula	collapseAssociativeFormulas()	This method collapses all associative operations appearing in this term, e.g.
Conjunction	combineWithAnd(Conjunctable f)	Returns a conjunction of this and the given formula.
Disjunction	combineWithOr(Disjunctable f)
ClassicalFormula	complement()
abstract boolean	equals(Object other)
abstract Set<Proposition>	getAtoms()	Processes the set of all atoms which appear in this formula
abstract Set<PlFormula>	getLiterals()	Returns all literals, i.e.
Set<PossibleWorld>	getModels()	Returns the set of models of this formula wrt.
abstract Set<PossibleWorld>	getModels(PlSignature sig)	Returns the set of models of this formula wrt.
Class<PlPredicate>	getPredicateCls()
abstract Set<PlPredicate>	getPredicates()	Processes the set of all predicates which appear in this formula
Collection<PlFormula>	getPrimeImplicants()	Returns the set of prime implicants of this formula.
PlSignature	getSignature()	Returns the signature of the language of this formula.
Probability	getUniformProbability()	Returns this formula's probability in the uniform distribution.
abstract int	hashCode()
boolean	isClause()	Checks whether this formula is a clause, i.e.
boolean	isConjunctiveClause()	Checks whether this formula is a conjunctive clause, i.e.
boolean	isLiteral()
abstract int	numberOfOccurrences(Proposition p)	Returns the number of occurrences of the given proposition within this formula
abstract PlFormula	replace(Proposition p, PlFormula f, int i)	Replaces the ith instance of the proposition p by f.
boolean	resolvableWith(PlFormula other)	Checks whether this formula (which must be a conjunction of literals) is resolvable with the given formula (which is also a conjunction of literals), i.e.
Conjunction	resolveWith(PlFormula other)	Resolves this formula with the given one (both have to be conjunctive clauses) and returns some resolvent.
PlFormula	toBlakeCanonicalForm()	This method returns this formula in Blake canonical form.
abstract Conjunction	toCnf()	This method returns this formula in conjunctive normal form (CNF).
PlFormula	toDnf()	This method returns this formula in disjunctive normal form (DNF).
abstract PlFormula	toNnf()	This method returns this formula in negation normal form (NNF).
abstract PlFormula	trim()	Removes duplicates (identical formulas) from conjunctions and disjunctions and removes duplicate negations.

Methods inherited from class java.lang.Object

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

Constructor Details

PlFormula

public PlFormula()

Default Constructor

Method Details

getPredicateCls

public Class<PlPredicate> getPredicateCls()

Specified by:

getPredicateCls in interface SimpleLogicalFormula

Returns:

The class description of the predicate used by this formula.

getSignature

public PlSignature getSignature()

Description copied from interface: Formula

Returns the signature of the language of this formula.

Specified by:

getSignature in interface Formula

Returns:

the signature of the language of this formula.

getAtoms

public abstract 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

Returns:

The set of all atoms

getLiterals

public abstract Set<PlFormula> getLiterals()

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

Returns:

all literals appearing in this formula.

combineWithAnd

public Conjunction combineWithAnd(Conjunctable f)

Description copied from interface: Conjunctable

Returns a conjunction of this and the given formula.

Specified by:

combineWithAnd in interface Conjunctable

Parameters:

f - a formula to be combined with AND and this.

Returns:

a conjunction of this and the given formula.

combineWithOr

public Disjunction combineWithOr(Disjunctable f)

Specified by:

combineWithOr in interface Disjunctable

Parameters:

f - a formula to be combined with OR and this.

Returns:

a disjunction of this and the given formula.

collapseAssociativeFormulas

public abstract PlFormula collapseAssociativeFormulas()

This method collapses all associative operations appearing in this term, e.g. every a||(b||c) becomes a||b||c.

Returns:

the collapsed formula.

getPredicates

public abstract 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

Returns:

all predicates that appear in this formula

trim

public abstract PlFormula trim()

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.

Returns:

an equivalent formula without duplicates.

getUniformProbability

public Probability getUniformProbability()

Returns this formula's probability in the uniform distribution.

Specified by:

getUniformProbability in interface ProbabilityAware

Returns:

this formula's probability in the uniform distribution.

toNnf

public abstract PlFormula toNnf()

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.

Returns:

the formula in NNF.

toCnf

public abstract Conjunction toCnf()

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.

Returns:

the formula in CNF.

toDnf

public PlFormula toDnf()

This method returns this formula in disjunctive normal form (DNF). A formula is in DNF iff it is a disjunction of conjunctive clauses. The DNF generated by this method is not necessarily minimal.

Returns:

the formula in DNF.

resolvableWith

public boolean resolvableWith(PlFormula other)

Checks whether this formula (which must be a conjunction of literals) is resolvable with the given formula (which is also a conjunction of literals), i.e. whether they contains exactly one complementary literal.

Parameters:

other - a conjunction of literals

Returns:

"true" iff this formula is resolvable with the other formula.

resolveWith

public Conjunction resolveWith(PlFormula other)

Resolves this formula with the given one (both have to be conjunctive clauses) and returns some resolvent.

Parameters:

other - a conjunction of formulas

Returns:

some resolvent.

toBlakeCanonicalForm

public PlFormula toBlakeCanonicalForm()

This method returns this formula in Blake canonical form. A formula is in Blake canonical form iff it is the disjunction of its prime implicants.

Returns:

the formula in Blake canonical form

getPrimeImplicants

public Collection<PlFormula> getPrimeImplicants()

Returns the set of prime implicants of this formula.

Returns:

the set of prime implicants of this formula.

getModels

public Set<PossibleWorld> getModels()

Returns the set of models of this formula wrt. a signature that only contains the propositions appearing in this formula.

Returns:

the set of models of this formula wrt. a signature that only contains the propositions appearing in this formula.

getModels

public abstract Set<PossibleWorld> getModels(PlSignature sig)

Returns the set of models of this formula wrt. the given signature.

Parameters:

sig - some propositional signature

Returns:

the set of models of this formula wrt. the given signature.

complement

public ClassicalFormula complement()

Specified by:

complement in interface Invertable

Returns:

the complement of this formula.

isClause

public boolean isClause()

Checks whether this formula is a clause, i.e. whether it is a disjunction of literals.

Returns:

"true" iff this formula is a clause.

isConjunctiveClause

public boolean isConjunctiveClause()

Checks whether this formula is a conjunctive clause, i.e. whether it is a conjunction of literals.

Returns:

"true" iff this formula is a conjunctive clause.

numberOfOccurrences

public abstract int numberOfOccurrences(Proposition p)

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

Parameters:

p - some proposition

Returns:

the number of occurrences of the given proposition within this formula

replace

public abstract PlFormula replace(Proposition p,
 PlFormula f,
 int i)

Replaces the ith instance of the proposition p by f.

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.

isLiteral

public boolean isLiteral()

Specified by:

isLiteral in interface SimpleLogicalFormula

Returns:

true if the formula represents a literal in the language or false otherwise

equals

public abstract boolean equals(Object other)

Specified by:

equals in interface SimpleLogicalFormula

Overrides:

equals in class Object

hashCode

public abstract int hashCode()

Specified by:

hashCode in interface SimpleLogicalFormula

Overrides:

hashCode in class Object

clone

public abstract PlFormula clone()

Description copied from interface: SimpleLogicalFormula

Creates a deep copy of this formula

Specified by:

clone in interface SimpleLogicalFormula

Returns:

the cloned formula