## Class 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()`
• ### 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()`
`java.util.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 net.sf.tweety.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, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait`
• ### 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, getUnboundVariables, isClosed, isClosed, isWellBound, isWellBound`
• ### Methods inherited from interface net.sf.tweety.logics.commons.syntax.interfaces.SimpleLogicalFormula

`equals, getPredicates, hashCode, isLiteral`
• ### Constructor Detail

• #### FolFormula

`public FolFormula()`
• ### Method Detail

• #### 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 java.util.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 java.lang.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:
`java.lang.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.