java.lang.Object
- net.sf.tweety.logics.commons.syntax.RelationalFormula
- - net.sf.tweety.logics.fol.syntax.FolFormula
  - - net.sf.tweety.logics.ml.syntax.MlFormula

All Implemented Interfaces:

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

Direct Known Subclasses:

Necessity, Possibility
```
public abstract class MlFormula
extends FolFormula
```
This class models a modal formula, i.e. it encapsulates an modal operator and a formula (either a modal formula or a FolFormula).

Author:

Matthias Thimm

Field Summary

Fields
Modifier and Type Field Description

private RelationalFormula formula
The inner formula of this modal formula

Constructor Summary

Constructors
Constructor Description

MlFormula(RelationalFormula formula)

Method Summary

Modifier and Type	Method	Description
`Conjunction`	`combineWithAnd(Conjunctable f)`	Returns a conjunction of this and the given formula.
`Disjunction`	`combineWithOr(Disjunctable f)`
`RelationalFormula`	`complement()`
`boolean`	`containsModalityOperator()`	Checks whether this formula contains a modal operator ("necessity" operator or "possibility" operator).
`boolean`	`containsQuantifier()`	Checks whether this formula contains any quantification.
`boolean`	`equals(java.lang.Object obj)`
`java.util.Set<FolAtom>`	`getAtoms()`	Processes the set of all atoms which appear in this formula
`RelationalFormula`	`getFormula()`	Returns the inner formula of this modal formula.
`java.util.Set<Functor>`	`getFunctors()`
`java.util.Set<? extends Predicate>`	`getPredicates()`	Processes the set of all predicates which appear in this formula
`java.util.Set<Variable>`	`getQuantifierVariables()`
`FolSignature`	`getSignature()`	Returns the signature of the language of this formula.
`java.util.Set<Term<?>>`	`getTerms()`
`<C extends Term<?>> java.util.Set<C>`	`getTerms(java.lang.Class<C> cls)`	Processes the set containing all terms of type C.
`java.util.Set<Variable>`	`getUnboundVariables()`
`Probability`	`getUniformProbability()`
`int`	`hashCode()`
`boolean`	`isClosed()`	Checks whether this formula is closed, i.e.
`boolean`	`isClosed(java.util.Set<Variable> boundVariables)`	Checks whether this formula is closed, i.e.
`boolean`	`isLiteral()`
`boolean`	`isWellBound()`	Checks whether this formula is well-bound, i.e.
`boolean`	`isWellBound(java.util.Set<Variable> boundVariables)`	Checks whether this formula is well-bound, i.e.

Methods inherited from class net.sf.tweety.logics.fol.syntax.FolFormula
clone, collapseAssociativeFormulas, isDnf, substitute, toDnf, toNnf

Methods inherited from class net.sf.tweety.logics.commons.syntax.RelationalFormula
allGroundInstances, allSubstitutions, containsTermsOfType, exchange, getPredicateCls, getSatisfactionRatio, isGround, isWellFormed, substitute, toString

Methods inherited from class java.lang.Object
finalize, getClass, notify, notifyAll, wait, wait, wait

- Field Detail
  - formula
```
private RelationalFormula formula
```
    The inner formula of this modal formula
- Constructor Detail
  - MlFormula
```
public MlFormula(RelationalFormula formula)
```
- Method Detail
  - getSignature
```
public FolSignature getSignature()
```
    Description copied from interface: Formula
    
    Returns the signature of the language of this formula.
    
    Specified by:
    
    getSignature in interface Formula
    
    Overrides:
    
    getSignature in class FolFormula
    
    Returns:
    
    the signature of the language of this formula.
  - getUniformProbability
```
public Probability getUniformProbability()
```
    Specified by:
    
    getUniformProbability in interface ProbabilityAware
    
    Overrides:
    
    getUniformProbability in class FolFormula
    
    Returns:
    
    this formula's probability in the uniform distribution.
  - getFormula
```
public RelationalFormula getFormula()
```
    Returns the inner formula of this modal formula.
    
    Specified by:
    
    getFormula in interface QuantifiedFormula
    
    Overrides:
    
    getFormula in class RelationalFormula
    
    Returns:
    
    the inner formula of this modal formula.
  - getPredicates
```
public java.util.Set<? extends Predicate> getPredicates()
```
    Description copied from interface: SimpleLogicalFormula
    
    Processes the set of all predicates which appear in this formula
    
    Returns:
    
    all predicates that appear in this formula
  - getFunctors
```
public java.util.Set<Functor> getFunctors()
```
    Specified by:
    
    getFunctors in class RelationalFormula
    
    Returns:
    
    all functors that appear in this formula.
  - getAtoms
```
public java.util.Set<FolAtom> getAtoms()
```
    Description copied from interface: SimpleLogicalFormula
    
    Processes the set of all atoms which appear in this formula
    
    Specified by:
    
    getAtoms in interface SimpleLogicalFormula
    
    Specified by:
    
    getAtoms in class RelationalFormula
    
    Returns:
    
    all atoms that appear in this formula.
  - containsQuantifier
```
public boolean containsQuantifier()
```
    Description copied from interface: QuantifiedFormula
    
    Checks whether this formula contains any quantification.
    
    Returns:
    
    "true" if this formula contains a quantification.
  - isClosed
```
public boolean isClosed()
```
    Description copied from interface: QuantifiedFormula
    
    Checks whether this formula is closed, i.e. whether every variables occurring in the formula is bound by a quantifier.
    
    Returns:
    
    "true" if this formula is closed, "false" otherwise.
  - isClosed
```
public boolean isClosed(java.util.Set<Variable> boundVariables)
```
    Description copied from interface: QuantifiedFormula
    
    Checks whether this formula is closed, i.e. whether every variables occurring in the formula is bound by a quantifier. Every variable in "boundVariables" is already assumed to be bound.
    
    Parameters:
    
    boundVariables - the variables assumed to be bound.
    
    Returns:
    
    "true" if this formula is closed wrt. "boundVariables", "false" otherwise.
  - getUnboundVariables
```
public java.util.Set<Variable> getUnboundVariables()
```
    Returns:
    
    a set of of unbound variables
  - isWellBound
```
public boolean isWellBound()
```
    Description copied from interface: QuantifiedFormula
    
    Checks whether this formula is well-bound, i.e. whether no variable bound by a quantifier is again bound by another quantifier within the first quantifier's range.
    
    Returns:
    
    "true" if this formula is well-bound, "false" otherwise.
  - isWellBound
```
public boolean isWellBound(java.util.Set<Variable> boundVariables)
```
    Description copied from interface: QuantifiedFormula
    
    Checks whether this formula is well-bound, i.e. whether no variable bound by a quantifier is again bound by another quantifier within the first quantifier range. Every variable in "boundVariables" is assumed to be bound already.
    
    Parameters:
    
    boundVariables - the variables assumed to be bound.
    
    Returns:
    
    "true" if this formula is well-bound, "false" otherwise.
  - 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
    
    Overrides:
    
    combineWithAnd in class FolFormula
    
    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
    
    Overrides:
    
    combineWithOr in class FolFormula
    
    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
    
    Overrides:
    
    complement in class FolFormula
    
    Returns:
    
    the complement of this formula.
  - isLiteral
```
public boolean isLiteral()
```
    Returns:
    
    true if the formula represents a literal in the language or false otherwise
  - getTerms
```
public java.util.Set<Term<?>> getTerms()
```
    Returns:
    
    a set containing all terms of this logical structure
  - getTerms
```
public <C extends Term<?>> java.util.Set<C> getTerms(java.lang.Class<C> cls)
```
    Description copied from interface: LogicStructure
    
    Processes the set containing all terms of type C. This method uses the equals method of the given Class and therefore does not add terms which are sub classes of type C to the set.
    
    Type Parameters:
    
    C - the type of terms
    
    Parameters:
    
    cls - The Class structure containing type information about the searched term
    
    Returns:
    
    A set containing all terms of type C of this logical structure
  - getQuantifierVariables
```
public java.util.Set<Variable> getQuantifierVariables()
```
    Specified by:
    
    getQuantifierVariables in interface QuantifiedFormula
    
    Overrides:
    
    getQuantifierVariables in class FolFormula
    
    Returns:
    
    a set containing all quantified variables
  - hashCode
```
public int hashCode()
```
    Specified by:
    
    hashCode in interface SimpleLogicalFormula
    
    Overrides:
    
    hashCode in class java.lang.Object
  - equals
```
public boolean equals(java.lang.Object obj)
```
    Specified by:
    
    equals in interface SimpleLogicalFormula
    
    Overrides:
    
    equals in class java.lang.Object
  - containsModalityOperator
```
public boolean containsModalityOperator()
```
    Checks whether this formula contains a modal operator ("necessity" operator or "possibility" operator).
    
    Returns:
    
    true if formula contains modality, false otherwise

Class MlFormula

Field Summary

Constructor Summary

Method Summary

Methods inherited from class net.sf.tweety.logics.fol.syntax.FolFormula

Methods inherited from class net.sf.tweety.logics.commons.syntax.RelationalFormula

Methods inherited from class java.lang.Object

Field Detail

formula

Constructor Detail

MlFormula

Method Detail

getSignature

getUniformProbability

getFormula

getPredicates

getFunctors

getAtoms

containsQuantifier

isClosed

isClosed

getUnboundVariables

isWellBound

isWellBound

combineWithAnd

combineWithOr

complement

isLiteral

getTerms

getTerms

getQuantifierVariables

hashCode

equals

containsModalityOperator