Package org.tweetyproject.logics.commons.syntax.interfaces

Interface QuantifiedFormula

All Superinterfaces:

ComplexLogicalFormula, Formula, LogicStructure, SimpleLogicalFormula

All Known Implementing Classes:

AssociativeFolFormula, Conjunction, Contradiction, DefaultRule, DefeasibleRule, DelpFact, DelpRule, Disjunction, Equivalence, ExclusiveDisjunction, ExistsQuantifiedFormula, FolAtom, FolFormula, ForallQuantifiedFormula, Implication, MlFormula, MlnFormula, Necessity, Negation, NLPNot, Possibility, RelationalConditional, RelationalFormula, RelationalProbabilisticConditional, SpecialFormula, StrictRule, Tautology

public interface QuantifiedFormula
extends ComplexLogicalFormula

Interface for a QuantifiedFormula with a set of quantified variables implementing an all- or exist-quantor for example.

Author:

Tim Janus

Method Summary

Modifier and Type	Method	Description
boolean	containsQuantifier()	Checks whether this formula contains any quantification.
SimpleLogicalFormula	getFormula()
Set<Variable>	getQuantifierVariables()
Set<Variable>	getUnboundVariables()
boolean	isClosed()	Checks whether this formula is closed, i.e.
boolean	isClosed(Set<Variable> boundVariables)	Checks whether this formula is closed, i.e.
boolean	isWellBound()	Checks whether this formula is well-bound, i.e.
boolean	isWellBound(Set<Variable> boundVariables)	Checks whether this formula is well-bound, i.e.

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

clone, exchange, isGround, isWellFormed, substitute, substitute

Methods inherited from interface org.tweetyproject.commons.Formula

getSignature

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

containsTermsOfType, getTerms, getTerms

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

equals, getAtoms, getPredicateCls, getPredicates, hashCode, isLiteral

Method Details

getFormula

SimpleLogicalFormula getFormula()

Returns:

the formula which is quantified

getQuantifierVariables

Set<Variable> getQuantifierVariables()

Returns:

a set containing all quantified variables

getUnboundVariables

Set<Variable> getUnboundVariables()

Returns:

a set of of unbound variables

containsQuantifier

boolean containsQuantifier()

Checks whether this formula contains any quantification.

Returns:

"true" if this formula contains a quantification.

isWellBound

boolean isWellBound()

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

boolean isWellBound(Set<Variable> boundVariables)

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.

isClosed

boolean isClosed()

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

boolean isClosed(Set<Variable> boundVariables)

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.