Class RelationalFormula
- java.lang.Object
-
- net.sf.tweety.logics.commons.syntax.RelationalFormula
-
- All Implemented Interfaces:
Formula
,ClassicalFormula
,ComplexLogicalFormula
,Conjunctable
,Disjunctable
,Invertable
,LogicStructure
,ProbabilityAware
,QuantifiedFormula
,SimpleLogicalFormula
- Direct Known Subclasses:
DefaultRule
,DelpRule
,FolFormula
,MlnFormula
,RelationalConditional
public abstract class RelationalFormula extends java.lang.Object implements ClassicalFormula, QuantifiedFormula
This is the abstract base class for relational formulas, i.e. formulas that are build on first-order signatures. NOTE: "RelationalFormula" and "FolFormula" differ in their meaning as follows:- A relational formula is any formula over a first-order signature, i.e. even a conditional
- A first-order formula is the actual first-order formula in the classical sense.
- Author:
- Matthias Thimm, Tim Janus, Anna Gessler
-
-
Constructor Summary
Constructors Constructor Description RelationalFormula()
-
Method Summary
Modifier and Type Method Description java.util.Set<RelationalFormula>
allGroundInstances(java.util.Set<Constant> constants)
Computes all ground instances of this relational formula wrt.java.util.Set<java.util.Map<Variable,Term<?>>>
allSubstitutions(java.util.Collection<? extends Term<?>> terms)
Computes all possible substitutions, i.e.abstract RelationalFormula
clone()
Creates a deep copy of this formulaabstract Disjunctable
combineWithAnd(Conjunctable f)
Returns a conjunction of this and the given formula.abstract Conjunctable
combineWithOr(Disjunctable f)
abstract RelationalFormula
complement()
<C extends Term<?>>
booleancontainsTermsOfType(java.lang.Class<C> cls)
Checks if this logical structure contains at least one term of type C.RelationalFormula
exchange(Term<?> v, Term<?> t)
Substitutes all occurrences of term "v" in this formula by term "t" and at the same time replaces all occurrences of term "t" by term "v" and eventually returns the new formula.abstract java.util.Set<? extends Atom>
getAtoms()
Processes the set of all atoms which appear in this formulaRelationalFormula
getFormula()
abstract java.util.Set<Functor>
getFunctors()
java.lang.Class<? extends Predicate>
getPredicateCls()
double
getSatisfactionRatio()
Returns the ratio of worlds not satisfying this formula to worlds satisfying this formula.abstract Probability
getUniformProbability()
boolean
isGround()
Checks whether this formula is ground, i.e.boolean
isWellFormed()
Tests whether this formula is well-formed, i.e.RelationalFormula
substitute(java.util.Map<? extends Term<?>,? extends Term<?>> map)
Substitutes all occurrences of all terms "v" in map.keyset() in this formula by map.get(v) and returns the new formula.
NOTE: variables bound to quantifiers are not substituted in their inner formulas even if they appear in the map.abstract RelationalFormula
substitute(Term<?> v, Term<?> t)
Substitutes all occurrences of term "v" in this formula by term "t" and returns the new formula.abstract java.lang.String
toString()
-
Methods inherited from class java.lang.Object
equals, getClass, hashCode, notify, notifyAll, wait, wait, wait
-
Methods inherited from interface net.sf.tweety.commons.Formula
getSignature
-
Methods inherited from interface net.sf.tweety.logics.commons.syntax.interfaces.LogicStructure
getTerms, getTerms
-
Methods inherited from interface net.sf.tweety.logics.commons.syntax.interfaces.QuantifiedFormula
containsQuantifier, getQuantifierVariables, getUnboundVariables, isClosed, isClosed, isWellBound, isWellBound
-
Methods inherited from interface net.sf.tweety.logics.commons.syntax.interfaces.SimpleLogicalFormula
equals, getPredicates, hashCode, isLiteral
-
-
-
-
Method Detail
-
getFormula
public RelationalFormula getFormula()
- Specified by:
getFormula
in interfaceQuantifiedFormula
- Returns:
- the relational formula
-
getAtoms
public abstract java.util.Set<? extends Atom> getAtoms()
Description copied from interface:SimpleLogicalFormula
Processes the set of all atoms which appear in this formula- Specified by:
getAtoms
in interfaceSimpleLogicalFormula
- Returns:
- all atoms that appear in this formula.
-
getFunctors
public abstract java.util.Set<Functor> getFunctors()
- Returns:
- all functors that appear in this formula.
-
getPredicateCls
public java.lang.Class<? extends Predicate> getPredicateCls()
- Specified by:
getPredicateCls
in interfaceSimpleLogicalFormula
- Returns:
- The class description of the predicate used by this formula.
-
substitute
public abstract RelationalFormula substitute(Term<?> v, Term<?> t) throws java.lang.IllegalArgumentException
Substitutes all occurrences of term "v" in this formula by term "t" and returns the new formula. NOTE: if "v" is a variable and bound to a quantifier then "v" is not substituted in that quantifiers inner formula.- Specified by:
substitute
in interfaceComplexLogicalFormula
- Parameters:
v
- the term to be substituted.t
- the term to substitute.- Returns:
- a formula where every occurrence of "v" is replaced by "t".
- Throws:
java.lang.IllegalArgumentException
- if "v" and "t" are of different sorts (NOTE: this exception is only thrown when "v" actually appears in this formula).
-
substitute
public RelationalFormula substitute(java.util.Map<? extends Term<?>,? extends Term<?>> map) throws java.lang.IllegalArgumentException
Substitutes all occurrences of all terms "v" in map.keyset() in this formula by map.get(v) and returns the new formula.
NOTE: variables bound to quantifiers are not substituted in their inner formulas even if they appear in the map.- Specified by:
substitute
in interfaceComplexLogicalFormula
- Parameters:
map
- a mapping defining which terms to be substituted.- Returns:
- a formula where every term in map.keyset() has been replaced by map.get(v).
- Throws:
java.lang.IllegalArgumentException
- if any term and its mapping are of different sorts (NOTE: this exception is only thrown when the variable actually appears in this formula).
-
exchange
public RelationalFormula exchange(Term<?> v, Term<?> t) throws java.lang.IllegalArgumentException
Substitutes all occurrences of term "v" in this formula by term "t" and at the same time replaces all occurrences of term "t" by term "v" and eventually returns the new formula. NOTE: if "v" is a variable and bound to a quantifier then "v" is not substituted in that quantifiers inner formula.- Specified by:
exchange
in interfaceComplexLogicalFormula
- Parameters:
v
- a term.t
- a term.- Returns:
- a new relational formula with both "v" and "t" exchanged.
- Throws:
java.lang.IllegalArgumentException
- if "v" and "t" are of different sorts
-
allSubstitutions
public java.util.Set<java.util.Map<Variable,Term<?>>> allSubstitutions(java.util.Collection<? extends Term<?>> terms) throws java.lang.IllegalArgumentException
Computes all possible substitutions, i.e. maps from variables to terms, of unbound variables of this formula to terms in "terms".- Parameters:
terms
- a set of terms.- Returns:
- a set of maps from variables to terms.
- Throws:
java.lang.IllegalArgumentException
- if there is an unbound variable in this formula for which there is no term in "terms" with the same sort.
-
allGroundInstances
public java.util.Set<RelationalFormula> allGroundInstances(java.util.Set<Constant> constants) throws java.lang.IllegalArgumentException
Computes all ground instances of this relational formula wrt. the given set of constants, i.e. every formula where each occurrence of some unbound variable is replaced by some constant.- Parameters:
constants
- a set of constants- Returns:
- a set of ground instances of this formula
- Throws:
java.lang.IllegalArgumentException
- if there is an unbound variable in this formula for which there is no constant in "constants" with the same sort.
-
getSatisfactionRatio
public double getSatisfactionRatio()
Returns the ratio of worlds not satisfying this formula to worlds satisfying this formula.- Returns:
- the ratio of worlds not satisfying this formula to worlds satisfying this formula.
-
getUniformProbability
public abstract Probability getUniformProbability()
- Specified by:
getUniformProbability
in interfaceProbabilityAware
- Returns:
- this formula's probability in the uniform distribution.
-
isGround
public boolean isGround()
Checks whether this formula is ground, i.e. whether there appears no variable in this formula.- Specified by:
isGround
in interfaceComplexLogicalFormula
- Returns:
- "true" if this formula is ground.
-
isWellFormed
public boolean isWellFormed()
Tests whether this formula is well-formed, i.e. whether
- there are no two variables with the same name but different sort
- there are no two constants with the same name but different sort
- there are no two predicates with the same name but different arguments
- there are no two functors with the same name but different sort or arguments
- every atom is complete, i.e. has a complete list of arguments
- every functional term is complete, i.e. has a complete list of arguments
- no variable bound by a quantifier is again bound by another quantifier within the first quantifier range.
- every functor has arity greater zero (otherwise it should be modeled by a constant- Specified by:
isWellFormed
in interfaceComplexLogicalFormula
- Returns:
- "true" if this formula is well-formed
-
containsTermsOfType
public <C extends Term<?>> boolean containsTermsOfType(java.lang.Class<C> cls)
Description copied from interface:LogicStructure
Checks if this logical structure contains at least one term of type C. This method is a shortcut for !getTerms(TermImplementation.class).isEmpty().- Specified by:
containsTermsOfType
in interfaceLogicStructure
- Type Parameters:
C
- the type of terms- Parameters:
cls
- The class structure representing the type C of the term.- Returns:
- True if this logical structure contains at least one term of type C or false otherwise.
-
complement
public abstract RelationalFormula complement()
- Specified by:
complement
in interfaceInvertable
- Returns:
- the complement of this formula.
-
combineWithOr
public abstract Conjunctable 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.
-
combineWithAnd
public abstract Disjunctable 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.
-
toString
public abstract java.lang.String toString()
- Overrides:
toString
in classjava.lang.Object
-
clone
public abstract RelationalFormula clone()
Description copied from interface:SimpleLogicalFormula
Creates a deep copy of this formula- Specified by:
clone
in interfaceComplexLogicalFormula
- Specified by:
clone
in interfaceSimpleLogicalFormula
- Returns:
- the cloned formula
-
-