Class RelationalFormula
java.lang.Object
org.tweetyproject.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 Object
implements ClassicalFormula, QuantifiedFormula
This is the abstract base class for relational formulas,
i.e. formulas that are build on firstorder signatures.
NOTE: "RelationalFormula" and "FolFormula" differ in their meaning as follows:
 A relational formula is any formula over a firstorder signature, i.e. even a conditional
 A firstorder formula is the actual firstorder formula in the classical sense.
 Author:
 Matthias Thimm, Tim Janus, Anna Gessler

Constructor Summary

Method Summary
Modifier and TypeMethodDescriptionallGroundInstances
(Set<Constant> constants) Computes all ground instances of this relational formula wrt.allSubstitutions
(Collection<? extends Term<?>> terms) Computes all possible substitutions, i.e.abstract RelationalFormula
clone()
Creates a deep copy of this formulaabstract Disjunctable
Returns a conjunction of this and the given formula.abstract Conjunctable
abstract RelationalFormula
<C extends Term<?>>
booleancontainsTermsOfType
(Class<C> cls) Checks if this logical structure contains at least one term of type C.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.getAtoms()
Processes the set of all atoms which appear in this formuladouble
Returns the ratio of worlds not satisfying this formula to worlds satisfying this formula.abstract Probability
boolean
isGround()
Checks whether this formula is ground, i.e.boolean
Tests whether this formula is wellformed, i.e.substitute
(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 String
toString()
Methods inherited from class java.lang.Object
equals, getClass, hashCode, notify, notifyAll, wait, wait, wait
Methods inherited from interface org.tweetyproject.commons.Formula
getSignature
Methods inherited from interface org.tweetyproject.logics.commons.syntax.interfaces.LogicStructure
getTerms, getTerms
Methods inherited from interface org.tweetyproject.logics.commons.syntax.interfaces.QuantifiedFormula
containsQuantifier, getQuantifierVariables, getUnboundVariables, isClosed, isClosed, isWellBound, isWellBound
Methods inherited from interface org.tweetyproject.logics.commons.syntax.interfaces.SimpleLogicalFormula
equals, getPredicates, hashCode, isLiteral

Constructor Details

RelationalFormula
public RelationalFormula()


Method Details

getFormula
 Specified by:
getFormula
in interfaceQuantifiedFormula
 Returns:
 the relational formula

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
 Returns:
 all functors that appear in this formula.

getPredicateCls
 Specified by:
getPredicateCls
in interfaceSimpleLogicalFormula
 Returns:
 The class description of the predicate used by this formula.

substitute
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:
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(Map<? extends Term<?>, ? extends Term<?>> map) throws IllegalArgumentExceptionSubstitutes 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:
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
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:
IllegalArgumentException
 if "v" and "t" are of different sorts

allSubstitutions
public Set<Map<Variable,Term<?>>> allSubstitutions(Collection<? extends Term<?>> terms) throws 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:
IllegalArgumentException
 if there is an unbound variable in this formula for which there is no term in "terms" with the same sort.

allGroundInstances
public Set<RelationalFormula> allGroundInstances(Set<Constant> constants) throws 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:
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
 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 wellformed, 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 wellformed

containsTermsOfType
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
 Specified by:
complement
in interfaceInvertable
 Returns:
 the complement of this 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.

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.

toString

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
