net.sf.tweety.logics.pl.syntax

Class PropositionalFormula

java.lang.Object

net.sf.tweety.logics.pl.syntax.PropositionalFormula

All Implemented Interfaces:

Formula, ClassicalFormula, Conjuctable, Disjunctable, Invertable, ProbabilityAware, SimpleLogicalFormula

Direct Known Subclasses:

AssociativePropositionalFormula, Negation, Proposition, SpecialFormula

public abstract class PropositionalFormula
extends java.lang.Object
implements ClassicalFormula

This class represents the common ancestor for propositional formulae.

Author:

Matthias Thimm, Tim Janus

Constructor Summary

Constructors

Constructor and Description
PropositionalFormula()

Method Summary

Modifier and Type	Method and Description
abstract PropositionalFormula	clone() Creates a deep copy of this formula
abstract PropositionalFormula	collapseAssociativeFormulas() This method collapses all associative operations appearing in this term, e.g.
Conjunction	combineWithAnd(Conjuctable f) Returns a conjunction of this and the given formula.
Disjunction	combineWithOr(Disjunctable f)
ClassicalFormula	complement()
abstract boolean	equals(java.lang.Object other)
abstract java.util.Set<Proposition>	getAtoms() Processes the set of all atoms which appear in this formula
abstract java.util.Set<PropositionalFormula>	getLiterals() Returns all literals, i.e.
java.util.Set<PossibleWorld>	getModels() Returns the set of models of this formula wrt.
abstract java.util.Set<PossibleWorld>	getModels(PropositionalSignature sig) Returns the set of models of this formula wrt.
java.lang.Class<PropositionalPredicate>	getPredicateCls()
abstract java.util.Set<PropositionalPredicate>	getPredicates() Processes the set of all predicates which appear in this formula
java.util.Collection<PropositionalFormula>	getPrimeImplicants() Returns the set of prime implicants of this formula.
PropositionalSignature	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 PropositionalFormula	replace(Proposition p, PropositionalFormula f, int i) Replaces the ith instance of the proposition p by f.
boolean	resolvableWith(PropositionalFormula other) Checks whether this formula (which must be a conjunction of literals) is resolvable with the given formulas (which is also a conjunction of literals, i.e.
Conjunction	resolveWith(PropositionalFormula other) Resolves this formula with the given one (both have to be conjunctive clauses) and returns some resolvent.
PropositionalFormula	toBlakeCanonicalForm() This method returns this formula in Blake canonical form.
abstract Conjunction	toCnf() This method returns this formula in conjunctive normal form (CNF).
PropositionalFormula	toDnf() This method returns this formula in disjunctive normal form (DNF).
abstract PropositionalFormula	toNnf() This method returns this formula in negation normal form (NNF).
abstract PropositionalFormula	trim() Removes duplicates (identical formulas) from conjunctions and disjunctions and duplicate negations.

Methods inherited from class java.lang.Object

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

Constructor Detail

PropositionalFormula

public PropositionalFormula()

Method Detail

getPredicateCls

public java.lang.Class<PropositionalPredicate> getPredicateCls()

Specified by:

getPredicateCls in interface SimpleLogicalFormula

Returns:

The class description of the predicate used by this formula.

getSignature

public PropositionalSignature 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 java.util.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 java.util.Set<PropositionalFormula> 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(Conjuctable f)

Description copied from interface: Conjuctable

Returns a conjunction of this and the given formula.

Specified by:

combineWithAnd in interface Conjuctable

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 PropositionalFormula 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 java.util.Set<PropositionalPredicate> 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 PropositionalFormula trim()

Removes duplicates (identical formulas) from conjunctions and disjunctions and duplicate negations.

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 PropositionalFormula 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.

Returns:

the formula in CNF.

toDnf

public PropositionalFormula toDnf()

This method returns this formula in disjunctive normal form (DNF). A formula is in DNF iff it is a disjunction of conjunctive clauses.

Returns:

the formula in DNF.

resolvableWith

public boolean resolvableWith(PropositionalFormula other)

Checks whether this formula (which must be a conjunction of literals) is resolvable with the given formulas (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(PropositionalFormula 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 PropositionalFormula 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 java.util.Collection<PropositionalFormula> getPrimeImplicants()

Returns the set of prime implicants of this formula.

Returns:

the set of prime implicants of this formula.

getModels

public java.util.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 java.util.Set<PossibleWorld> getModels(PropositionalSignature 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 PropositionalFormula replace(Proposition p,
                                             PropositionalFormula 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(java.lang.Object other)

Specified by:

equals in interface SimpleLogicalFormula

Overrides:

equals in class java.lang.Object

hashCode

public abstract int hashCode()

Specified by:

hashCode in interface SimpleLogicalFormula

Overrides:

hashCode in class java.lang.Object

clone

public abstract PropositionalFormula clone()

Description copied from interface: SimpleLogicalFormula

Creates a deep copy of this formula

Specified by:

clone in interface SimpleLogicalFormula

Overrides:

clone in class java.lang.Object