Package org.tweetyproject.logics.fol.syntax

Class FolFormula

java.lang.Object

org.tweetyproject.logics.commons.syntax.RelationalFormula

org.tweetyproject.logics.fol.syntax.FolFormula

All Implemented Interfaces:

Formula, ClassicalFormula, ComplexLogicalFormula, Conjunctable, Disjunctable, Invertable, LogicStructure, ProbabilityAware, QuantifiedFormula, SimpleLogicalFormula

Direct Known Subclasses:

AssociativeFolFormula, Equivalence, ExistsQuantifiedFormula, FolAtom, ForallQuantifiedFormula, Implication, MlFormula, Negation, NLPNot, SpecialFormula

public abstract class FolFormula
extends RelationalFormula

The common abstract class for formulas of first-order logic. 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

Constructor Summary

Constructors

Constructor	Description
FolFormula()	Default

Method Summary

Modifier and Type	Method	Description
abstract FolFormula	clone()	Creates a deep copy of this formula
abstract RelationalFormula	collapseAssociativeFormulas()	This method collapses all associative operations appearing in this term, e.g.
Conjunction	combineWithAnd(Conjunctable f)	Returns a conjunction of this and the given formula.
Disjunction	combineWithOr(Disjunctable f)
RelationalFormula	complement()
Set<Variable>	getQuantifierVariables()
FolSignature	getSignature()	Returns the signature of the language of this formula.
Probability	getUniformProbability()
abstract boolean	isDnf()	Checks whether this formula is in disjunctive normal form.
abstract FolFormula	substitute(Term<?> v, Term<?> t)	Substitutes all occurrences of term "v" in this formula by term "t" and returns the new formula.
FolFormula	toDnf()	Makes a disjunctive normal form of this formula.
abstract FolFormula	toNnf()	Makes the negation normal form of this formula.

Methods inherited from class org.tweetyproject.logics.commons.syntax.RelationalFormula

allGroundInstances, allSubstitutions, containsTermsOfType, exchange, getAtoms, getFormula, getFunctors, getPredicateCls, getSatisfactionRatio, isGround, isWellFormed, substitute, toString

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, wait, wait, wait

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, getUnboundVariables, isClosed, isClosed, isWellBound, isWellBound

Methods inherited from interface org.tweetyproject.logics.commons.syntax.interfaces.SimpleLogicalFormula

equals, getPredicates, hashCode, isLiteral

Constructor Details

FolFormula

public FolFormula()

Default

Method Details

combineWithAnd

public Conjunction combineWithAnd(Conjunctable f)

Description copied from interface: Conjunctable

Returns a conjunction of this and the given formula.

Specified by:

combineWithAnd in interface Conjunctable

Specified by:

combineWithAnd in class RelationalFormula

Parameters:

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

Returns:

a conjunction of this and the given formula.

combineWithOr

public Disjunction combineWithOr(Disjunctable f)

Specified by:

combineWithOr in interface Disjunctable

Specified by:

combineWithOr in class RelationalFormula

Parameters:

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

Returns:

a disjunction of this and the given formula.

complement

public RelationalFormula complement()

Specified by:

complement in interface Invertable

Specified by:

complement in class RelationalFormula

Returns:

the complement of this formula.

getQuantifierVariables

public Set<Variable> getQuantifierVariables()

Returns:

a set containing all quantified variables

toDnf

public FolFormula toDnf()

Makes a disjunctive normal form of this formula.

Returns:

the DNF of this formula

toNnf

public abstract FolFormula toNnf()

Makes the negation normal form of this formula.

Returns:

the NNF of this formula

collapseAssociativeFormulas

public abstract RelationalFormula 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.

getUniformProbability

public Probability getUniformProbability()

Specified by:

getUniformProbability in interface ProbabilityAware

Specified by:

getUniformProbability in class RelationalFormula

Returns:

this formula's probability in the uniform distribution.

isDnf

public abstract boolean isDnf()

Checks whether this formula is in disjunctive normal form.

Returns:

"true" iff this formula is in disjunctive normal form.

substitute

public abstract FolFormula substitute(Term<?> v,
 Term<?> t)
                               throws IllegalArgumentException

Description copied from class: RelationalFormula

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

Specified by:

substitute in class RelationalFormula

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).

clone

public abstract FolFormula 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

Specified by:

clone in class RelationalFormula

Returns:

the cloned formula

getSignature

public FolSignature getSignature()

Description copied from interface: Formula

Returns the signature of the language of this formula.

Returns:

the signature of the language of this formula.