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

Interface ComplexLogicalFormula

All Superinterfaces:
Formula, LogicStructure, SimpleLogicalFormula
All Known Subinterfaces:
QuantifiedFormula
All Known Implementing Classes:
AbaElement, AbaRule, AggregateAtom, AggregateElement, AggregateHead, ASPAtom, ASPBodyElement, ASPElement, ASPHead, ASPLiteral, ASPRule, AssociativeFolFormula, AssociativeFormulaSupport, Assumption, ChoiceElement, ChoiceHead, ClassicalHead, ComparativeAtom, ComplexLogicalFormulaAdapter, Conjunction, Contradiction, DefaultNegation, DefaultRule, DefeasibleInferenceRule, DefeasibleRule, DelpFact, DelpRule, Disjunction, Equivalence, ExclusiveDisjunction, ExistsQuantifiedFormula, FolAtom, FolFormula, ForallQuantifiedFormula, Implication, InferenceRule, InferenceRule, MlFormula, MlnFormula, Necessity, Negation, Negation, NLPNot, NLPRule, OptimizationElement, OptimizationStatement, Possibility, RelationalConditional, RelationalFormula, RelationalProbabilisticConditional, SpecialFormula, StrictInferenceRule, StrictNegation, StrictRule, Tautology
public interface ComplexLogicalFormula extends SimpleLogicalFormula, LogicStructure
A complex logical formula can contain arguments referred as terms, this interface provides methods to substitute and exchange those terms. It also provides utility functions like isGround() and isWellFormed().
Author:
Tim Janus, Matthias Thimm

  • Method Details

    • substitute

      ComplexLogicalFormula substitute(Term<?> v, Term<?> t) throws IllegalArgumentException
      Substitutes all occurrences of term "v" in this formula by term "t" and returns the new formula.
      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

    • substitute

      ComplexLogicalFormula substitute(Map<? extends Term<?>,? extends Term<?>> map) throws IllegalArgumentException
      Substitutes all occurrences of all terms "v" in map.keyset() in this formula by map.get(v) and returns the new formula.
      Parameters:
      map - a mapping defining which terms to be substituted.
      Returns:
      a formula where every term in map.keyset() has been replaced by map.get(v).
      Throws:
      IllegalArgumentException - if any term and its mapping are of different sorts

    • exchange

      ComplexLogicalFormula exchange(Term<?> v, Term<?> t) throws IllegalArgumentException
      Substitutes all occurrences of term "v" in this formula by term "t" and at the same time replaces all occurrences of term "t" by term "v" and eventually returns the new formula.
      Parameters:
      v - a term.
      t - a term.
      Returns:
      a new logical formula with both "v" and "t" exchanged.
      Throws:
      IllegalArgumentException - if "v" and "t" are of different sorts

    • isGround

      boolean isGround()
      Checks whether this formula is ground, i.e. whether there appears no variable in this formula.
      Returns:
      "true" if this formula is ground.

    • isWellFormed

      boolean isWellFormed()
      Checks if this formula is well formed in the logical langauge. What well- formed means is highly language dependent and the documentation of implementing sub classes shall describe the well formed term for the language they model.
      Returns:
      true if the formula is well-formed, false otherwise

    • clone

      ComplexLogicalFormula clone()
      Description copied from interface: SimpleLogicalFormula
      Creates a deep copy of this formula
      Specified by:
      clone in interface SimpleLogicalFormula
      Returns:
      the cloned formula