Package org.tweetyproject.logics.commons.syntax

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 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
Set<RelationalFormula>	allGroundInstances(Set<Constant> constants)	Computes all ground instances of this relational formula wrt.
Set<Map<Variable,Term<?>>>	allSubstitutions(Collection<? extends Term<?>> terms)	Computes all possible substitutions, i.e.
abstract RelationalFormula	clone()	Creates a deep copy of this formula
abstract Disjunctable	combineWithAnd(Conjunctable f)	Returns a conjunction of this and the given formula.
abstract Conjunctable	combineWithOr(Disjunctable f)
abstract RelationalFormula	complement()
<C extends Term<?>> boolean	containsTermsOfType(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 Set<? extends Atom>	getAtoms()	Processes the set of all atoms which appear in this formula
RelationalFormula	getFormula()
abstract Set<Functor>	getFunctors()
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(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

public RelationalFormula getFormula()

Specified by:

getFormula in interface QuantifiedFormula

Returns:

the relational formula

getAtoms

public abstract Set<? extends Atom> getAtoms()

Description copied from interface: SimpleLogicalFormula

Processes the set of all atoms which appear in this formula

Specified by:

getAtoms in interface SimpleLogicalFormula

Returns:

all atoms that appear in this formula.

getFunctors

public abstract Set<Functor> getFunctors()

Returns:

all functors that appear in this formula.

getPredicateCls

public Class<? extends Predicate> getPredicateCls()

Specified by:

getPredicateCls in interface SimpleLogicalFormula

Returns:

The class description of the predicate used by this formula.

substitute

public abstract RelationalFormula substitute(Term<?> v,
 Term<?> t)
                                      throws 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 interface ComplexLogicalFormula

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 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 interface ComplexLogicalFormula

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

public RelationalFormula exchange(Term<?> v,
 Term<?> t)
                           throws 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 interface ComplexLogicalFormula

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

public abstract Probability getUniformProbability()

Specified by:

getUniformProbability in interface ProbabilityAware

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 interface ComplexLogicalFormula

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 interface ComplexLogicalFormula

Returns:

"true" if this formula is well-formed

containsTermsOfType

public <C extends Term<?>> boolean containsTermsOfType(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 interface LogicStructure

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 interface Invertable

Returns:

the complement of this formula.

combineWithOr

public abstract Conjunctable combineWithOr(Disjunctable f)

Specified by:

combineWithOr in interface Disjunctable

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 interface Conjunctable

Parameters:

f - a formula to be combined with AND and this.

Returns:

a conjunction of this and the given formula.

toString

public abstract String toString()

Overrides:

toString in class Object

clone

public abstract RelationalFormula clone()

Description copied from interface: SimpleLogicalFormula

Creates a deep copy of this formula

Specified by:

clone in interface ComplexLogicalFormula

Specified by:

clone in interface SimpleLogicalFormula

Returns:

the cloned formula