net.sf.tweety.logics.commons.syntax.interfaces

Interface QuantifiedFormula

All Superinterfaces:

ComplexLogicalFormula, Formula, LogicStructure, SimpleLogicalFormula

All Known Implementing Classes:

AssociativeFOLFormula, Conjunction, Contradiction, DefaultRule, DefeasibleRule, DelpFact, DelpRule, Disjunction, ExistsQuantifiedFormula, FOLAtom, FolFormula, ForallQuantifiedFormula, MlnFormula, ModalFormula, Necessity, Negation, NLPNot, Possibility, QuantifiedFormula, 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 and Description
boolean	containsQuantifier() Checks whether this formula contains any quantification.
SimpleLogicalFormula	getFormula()
java.util.Set<Variable>	getQuantifierVariables()
java.util.Set<Variable>	getUnboundVariables()
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	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 interface net.sf.tweety.logics.commons.syntax.interfaces.ComplexLogicalFormula

clone, exchange, isGround, isWellFormed, substitute, substitute

Methods inherited from interface net.sf.tweety.logics.commons.syntax.interfaces.SimpleLogicalFormula

equals, getAtoms, getPredicateCls, getPredicates, hashCode, isLiteral

Methods inherited from interface net.sf.tweety.commons.Formula

getSignature

Methods inherited from interface net.sf.tweety.logics.commons.syntax.interfaces.LogicStructure

containsTermsOfType, getTerms, getTerms

Method Detail

getFormula

SimpleLogicalFormula getFormula()

Returns:

the formula which is quantified

getQuantifierVariables

java.util.Set<Variable> getQuantifierVariables()

Returns:

a set containing all quantified variables

getUnboundVariables

java.util.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(java.util.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(java.util.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.