Package net.sf.tweety.logics.pl.syntax
Class SpecialFormula
- java.lang.Object
-
- net.sf.tweety.logics.pl.syntax.PlFormula
-
- net.sf.tweety.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()
-
Method Summary
Modifier and Type Method Description PlFormula
collapseAssociativeFormulas()
This method collapses all associative operations appearing in this term, e.g.java.util.Set<Proposition>
getAtoms()
Processes the set of all atoms which appear in this formulajava.util.Set<PlFormula>
getLiterals()
Returns all literals, i.e.java.util.Set<PlPredicate>
getPredicates()
Processes the set of all predicates which appear in this formulaint
numberOfOccurrences(Proposition p)
Returns the number of occurrences of the given proposition within this formulaPlFormula
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 net.sf.tweety.logics.pl.syntax.PlFormula
clone, combineWithAnd, combineWithOr, complement, equals, getModels, getModels, getPredicateCls, getPrimeImplicants, getSignature, getUniformProbability, hashCode, isClause, isConjunctiveClause, isLiteral, resolvableWith, resolveWith, toBlakeCanonicalForm, toDnf
-
-
-
-
Method Detail
-
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 classPlFormula
- Returns:
- the collapsed formula.
-
getPredicates
public 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
- Specified by:
getPredicates
in classPlFormula
- 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.
-
getAtoms
public 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
- Specified by:
getAtoms
in classPlFormula
- Returns:
- The set of all atoms
-
getLiterals
public java.util.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 classPlFormula
- 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.
-
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 classPlFormula
- 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.
-
-