Package org.tweetyproject.logics.ml.syntax

Class Necessity

java.lang.Object

org.tweetyproject.logics.commons.syntax.RelationalFormula

org.tweetyproject.logics.fol.syntax.FolFormula

org.tweetyproject.logics.ml.syntax.MlFormula

org.tweetyproject.logics.ml.syntax.Necessity

All Implemented Interfaces:

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

public class Necessity
extends MlFormula

This class models the necessity modality.

Author:

Matthias Thimm

Constructor Summary

Constructors

Constructor	Description
Necessity(RelationalFormula formula)	Creates a new necessity formula with the given inner formula

Method Summary

Modifier and Type	Method	Description
FolFormula	clone()	Creates a deep copy of this formula
RelationalFormula	collapseAssociativeFormulas()	This method collapses all associative operations appearing in this term, e.g.
boolean	isDnf()	Checks whether this formula is in disjunctive normal form.
FolFormula	substitute(Term<?> v, Term<?> t)	Substitutes all occurrences of term "v" in this formula by term "t" and returns the new formula.
FolFormula	toNnf()	Makes the negation normal form of this formula.
String	toString()

Methods inherited from class org.tweetyproject.logics.ml.syntax.MlFormula

combineWithAnd, combineWithOr, complement, containsModalityOperator, containsQuantifier, equals, getAtoms, getFormula, getFunctors, getPredicates, getQuantifierVariables, getSignature, getTerms, getTerms, getUnboundVariables, getUniformProbability, hashCode, isClosed, isClosed, isLiteral, isWellBound, isWellBound

Methods inherited from class org.tweetyproject.logics.fol.syntax.FolFormula

toDnf

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

allGroundInstances, allSubstitutions, containsTermsOfType, exchange, getPredicateCls, getSatisfactionRatio, isGround, isWellFormed, substitute

Methods inherited from class java.lang.Object

getClass, notify, notifyAll, wait, wait, wait

Constructor Details

Necessity

public Necessity(RelationalFormula formula)

Creates a new necessity formula with the given inner formula

Parameters:

formula - a formula, either a modal formula or a first-order formula.

Method Details

substitute

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

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

toString

public String toString()

Specified by:

toString in class RelationalFormula

clone

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

Returns:

the cloned formula

toNnf

public FolFormula toNnf()

Description copied from class: FolFormula

Makes the negation normal form of this formula.

Specified by:

toNnf in class FolFormula

Returns:

the NNF of this formula

isDnf

public boolean isDnf()

Description copied from class: FolFormula

Checks whether this formula is in disjunctive normal form.

Specified by:

isDnf in class FolFormula

Returns:

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

collapseAssociativeFormulas

public RelationalFormula collapseAssociativeFormulas()

Description copied from class: FolFormula

This method collapses all associative operations appearing in this term, e.g. every a||(b||c) becomes a||b||c.

Specified by:

collapseAssociativeFormulas in class FolFormula

Returns:

the collapsed formula.