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