net.sf.tweety.logics.el.syntax

Class Necessity

java.lang.Object

net.sf.tweety.logics.fol.syntax.RelationalFormula

net.sf.tweety.logics.el.syntax.ModalFormula

net.sf.tweety.logics.el.syntax.Necessity

All Implemented Interfaces:

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

public class Necessity
extends ModalFormula

This class models the necessity modality.

Author:

Matthias Thimm

Constructor Summary

Constructors

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

Method Summary

Modifier and Type	Method and Description
RelationalFormula	clone() Creates a deep copy of this formula
RelationalFormula	substitute(Term<?> v, Term<?> t) Substitutes all occurrences of term "v" in this formula by term "t" and returns the new formula.
java.lang.String	toString()

Methods inherited from class net.sf.tweety.logics.el.syntax.ModalFormula

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

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

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

Methods inherited from class java.lang.Object

finalize, getClass, notify, notifyAll, wait, wait, wait

Constructor Detail

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 Detail

substitute

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

Overrides:

substitute in class ModalFormula

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

toString

public java.lang.String toString()

Specified by:

toString in class RelationalFormula

clone

public 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

Specified by:

clone in class RelationalFormula