public abstract class PropositionalFormula extends java.lang.Object implements ClassicalFormula
Constructor and Description |
---|
PropositionalFormula() |
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 |
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.
|
public java.lang.Class<PropositionalPredicate> getPredicateCls()
getPredicateCls
in interface SimpleLogicalFormula
public PropositionalSignature getSignature()
Formula
getSignature
in interface Formula
public abstract java.util.Set<Proposition> getAtoms()
SimpleLogicalFormula
getAtoms
in interface SimpleLogicalFormula
public abstract java.util.Set<PropositionalFormula> getLiterals()
public Conjunction combineWithAnd(Conjuctable f)
Conjuctable
combineWithAnd
in interface Conjuctable
f
- a formula to be combined with AND and this.public Disjunction combineWithOr(Disjunctable f)
combineWithOr
in interface Disjunctable
f
- a formula to be combined with OR and this.public abstract PropositionalFormula collapseAssociativeFormulas()
public abstract java.util.Set<PropositionalPredicate> getPredicates()
SimpleLogicalFormula
getPredicates
in interface SimpleLogicalFormula
public abstract PropositionalFormula trim()
public Probability getUniformProbability()
getUniformProbability
in interface ProbabilityAware
public abstract PropositionalFormula toNnf()
public abstract Conjunction toCnf()
public PropositionalFormula toDnf()
public boolean resolvableWith(PropositionalFormula other)
other
- a conjunction of literalspublic Conjunction resolveWith(PropositionalFormula other)
other
- a conjunction of formulaspublic PropositionalFormula toBlakeCanonicalForm()
public java.util.Collection<PropositionalFormula> getPrimeImplicants()
public java.util.Set<PossibleWorld> getModels()
public abstract java.util.Set<PossibleWorld> getModels(PropositionalSignature sig)
sig
- some propositional signaturepublic ClassicalFormula complement()
complement
in interface Invertable
public boolean isConjunctiveClause()
public abstract int numberOfOccurrences(Proposition p)
p
- some propositionpublic abstract PropositionalFormula replace(Proposition p, PropositionalFormula f, int i)
p
- some propositionf
- some formulai
- the index of the propositionpublic boolean isLiteral()
isLiteral
in interface SimpleLogicalFormula
public abstract boolean equals(java.lang.Object other)
equals
in interface SimpleLogicalFormula
equals
in class java.lang.Object
public abstract int hashCode()
hashCode
in interface SimpleLogicalFormula
hashCode
in class java.lang.Object
public abstract PropositionalFormula clone()
SimpleLogicalFormula
clone
in interface SimpleLogicalFormula
clone
in class java.lang.Object