Package net.sf.tweety.logics.pl.syntax
Class PlFormula
- java.lang.Object
-
- net.sf.tweety.logics.pl.syntax.PlFormula
-
- All Implemented Interfaces:
Formula
,ClassicalFormula
,Conjunctable
,Disjunctable
,Invertable
,ProbabilityAware
,SimpleLogicalFormula
- Direct Known Subclasses:
AssociativePlFormula
,Equivalence
,ExistsQuantifiedFormula
,ForallQuantifiedFormula
,Implication
,Negation
,Proposition
,SpecialFormula
public abstract class PlFormula extends java.lang.Object implements ClassicalFormula
This class represents the common ancestor for propositional formulae.- Author:
- Matthias Thimm, Tim Janus
-
-
Constructor Summary
Constructors Constructor Description PlFormula()
-
Method Summary
Modifier and Type Method Description abstract PlFormula
clone()
Creates a deep copy of this formulaabstract 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(java.lang.Object other)
abstract java.util.Set<Proposition>
getAtoms()
Processes the set of all atoms which appear in this formulaabstract java.util.Set<PlFormula>
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(PlSignature sig)
Returns the set of models of this formula wrt.java.lang.Class<PlPredicate>
getPredicateCls()
abstract java.util.Set<PlPredicate>
getPredicates()
Processes the set of all predicates which appear in this formulajava.util.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 formulaabstract 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 formulas (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.
-
-
-
Method Detail
-
getPredicateCls
public java.lang.Class<PlPredicate> getPredicateCls()
- Specified by:
getPredicateCls
in interfaceSimpleLogicalFormula
- 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 interfaceFormula
- 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 interfaceSimpleLogicalFormula
- Returns:
- The set of all atoms
-
getLiterals
public abstract java.util.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 interfaceConjunctable
- 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 interfaceDisjunctable
- 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 java.util.Set<PlPredicate> getPredicates()
Description copied from interface:SimpleLogicalFormula
Processes the set of all predicates which appear in this formula- Specified by:
getPredicates
in interfaceSimpleLogicalFormula
- 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 interfaceProbabilityAware
- 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.- 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.- 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 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(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 java.util.Collection<PlFormula> 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(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 interfaceInvertable
- 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 propositionf
- some formulai
- 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 interfaceSimpleLogicalFormula
- 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 interfaceSimpleLogicalFormula
- Overrides:
equals
in classjava.lang.Object
-
hashCode
public abstract int hashCode()
- Specified by:
hashCode
in interfaceSimpleLogicalFormula
- Overrides:
hashCode
in classjava.lang.Object
-
clone
public abstract PlFormula clone()
Description copied from interface:SimpleLogicalFormula
Creates a deep copy of this formula- Specified by:
clone
in interfaceSimpleLogicalFormula
- Returns:
- the cloned formula
-
-