Package net.sf.tweety.logics.pl.syntax
Class Negation
- java.lang.Object
-
- net.sf.tweety.logics.pl.syntax.PlFormula
-
- net.sf.tweety.logics.pl.syntax.Negation
-
- All Implemented Interfaces:
Formula
,ClassicalFormula
,Conjunctable
,Disjunctable
,Invertable
,ProbabilityAware
,SimpleLogicalFormula
public class Negation extends PlFormula
This class models classical negation of propositional logic.- Author:
- Matthias Thimm, Tim Janus
-
-
Method Summary
Modifier and Type Method Description PlFormula
clone()
Creates a deep copy of this formulaPlFormula
collapseAssociativeFormulas()
This method collapses all associative operations appearing in this term, e.g.boolean
equals(java.lang.Object obj)
java.util.Set<Proposition>
getAtoms()
Processes the set of all atoms which appear in this formulaPlFormula
getFormula()
Returns the formula within this negation.java.util.Set<PlFormula>
getLiterals()
Returns all literals, i.e.java.util.Set<PossibleWorld>
getModels(PlSignature sig)
Returns the set of models of this formula wrt.java.util.Set<PlPredicate>
getPredicates()
Processes the set of all predicates which appear in this formulaPlSignature
getSignature()
Returns the signature of the language of this formula.int
hashCode()
boolean
hasLowerBindingPriority(PlFormula other)
boolean
isLiteral()
int
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).java.lang.String
toString()
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
combineWithAnd, combineWithOr, complement, getModels, getPredicateCls, getPrimeImplicants, getUniformProbability, isClause, isConjunctiveClause, resolvableWith, resolveWith, toBlakeCanonicalForm, toDnf
-
-
-
-
Constructor Detail
-
Negation
public Negation(PlFormula formula)
Creates a new negation with the given formula.- Parameters:
formula
- the formula within the negation.
-
-
Method Detail
-
getFormula
public PlFormula getFormula()
Returns the formula within this negation.- Returns:
- the formula within this negation.
-
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.
-
hasLowerBindingPriority
public boolean hasLowerBindingPriority(PlFormula other)
-
toString
public java.lang.String toString()
- Overrides:
toString
in classjava.lang.Object
-
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.
-
trim
public PlFormula trim()
Description copied from class:PlFormula
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.
-
hashCode
public int hashCode()
- Specified by:
hashCode
in interfaceSimpleLogicalFormula
- Specified by:
hashCode
in classPlFormula
-
equals
public boolean equals(java.lang.Object obj)
- Specified by:
equals
in interfaceSimpleLogicalFormula
- Specified by:
equals
in classPlFormula
-
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
-
clone
public PlFormula clone()
Description copied from interface:SimpleLogicalFormula
Creates a deep copy of this formula- Specified by:
clone
in interfaceSimpleLogicalFormula
- Specified by:
clone
in classPlFormula
- Returns:
- the cloned formula
-
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
-
isLiteral
public boolean isLiteral()
- Specified by:
isLiteral
in interfaceSimpleLogicalFormula
- Overrides:
isLiteral
in classPlFormula
- Returns:
- true if the formula represents a literal in the language or false otherwise
-
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.
-
getSignature
public PlSignature getSignature()
Description copied from interface:Formula
Returns the signature of the language of this formula.- Specified by:
getSignature
in interfaceFormula
- Overrides:
getSignature
in classPlFormula
- Returns:
- the signature of the language of 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.
-
getModels
public java.util.Set<PossibleWorld> getModels(PlSignature sig)
Description copied from class:PlFormula
Returns the set of models of this formula wrt. the given signature.
-
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.
-
-