Class PlFormula
java.lang.Object
org.tweetyproject.logics.pl.syntax.PlFormula
- All Implemented Interfaces:
Formula
,ClassicalFormula
,Conjunctable
,Disjunctable
,Invertable
,ProbabilityAware
,SimpleLogicalFormula
- Direct Known Subclasses:
AssociativePlFormula
,Equivalence
,ExistsQuantifiedFormula
,ForallQuantifiedFormula
,Implication
,Indecision
,Negation
,Proposition
,SpecialFormula
,WeakNegation
This class represents the common ancestor for propositional formulae.
- Author:
- Matthias Thimm, Tim Janus
-
Constructor Summary
-
Method Summary
Modifier and TypeMethodDescriptionabstract PlFormula
clone()
Creates a deep copy of this formulaabstract PlFormula
This method collapses all associative operations appearing in this term, e.g.Returns a conjunction of this and the given formula.abstract boolean
abstract Set<Proposition>
getAtoms()
Processes the set of all atoms which appear in this formulaReturns all literals, i.e.Returns the set of models of this formula wrt.abstract Set<PossibleWorld>
getModels
(PlSignature sig) Returns the set of models of this formula wrt.abstract Set<PlPredicate>
Processes the set of all predicates which appear in this formulaReturns the set of prime implicants of this formula.Returns the signature of the language of this formula.Returns this formula's probability in the uniform distribution.abstract int
hashCode()
boolean
isClause()
Checks whether this formula is a clause, i.e.boolean
Checks whether this formula is a conjunctive clause, i.e.boolean
abstract int
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 formula (which is also a conjunction of literals), i.e.resolveWith
(PlFormula other) Resolves this formula with the given one (both have to be conjunctive clauses) and returns some resolvent.This method returns this formula in Blake canonical form.abstract Conjunction
toCnf()
This method returns this formula in conjunctive normal form (CNF).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.
-
Constructor Details
-
PlFormula
public PlFormula()
-
-
Method Details
-
getPredicateCls
- Specified by:
getPredicateCls
in interfaceSimpleLogicalFormula
- Returns:
- The class description of the predicate used by this formula.
-
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
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
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
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
- 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
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
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
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
Returns this formula's probability in the uniform distribution.- Specified by:
getUniformProbability
in interfaceProbabilityAware
- Returns:
- this formula's probability in the uniform distribution.
-
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
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. The CNF generated by this method is not necessarily minimal.- Returns:
- the formula in CNF.
-
toDnf
This method returns this formula in disjunctive normal form (DNF). A formula is in DNF iff it is a disjunction of conjunctive clauses. The DNF generated by this method is not necessarily minimal.- Returns:
- the formula in DNF.
-
resolvableWith
Checks whether this formula (which must be a conjunction of literals) is resolvable with the given formula (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
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
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
Returns the set of prime implicants of this formula.- Returns:
- the set of prime implicants of this formula.
-
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
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
- 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
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
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
- Specified by:
equals
in interfaceSimpleLogicalFormula
- Overrides:
equals
in classObject
-
hashCode
public abstract int hashCode()- Specified by:
hashCode
in interfaceSimpleLogicalFormula
- Overrides:
hashCode
in classObject
-
clone
Description copied from interface:SimpleLogicalFormula
Creates a deep copy of this formula- Specified by:
clone
in interfaceSimpleLogicalFormula
- Returns:
- the cloned formula
-