Class HerbrandInterpretation

All Implemented Interfaces:
Iterable<FolAtom>, Collection<FolAtom>, Interpretation<FolBeliefSet,​FolFormula>

public class HerbrandInterpretation extends InterpretationSet<FolAtom,​FolBeliefSet,​FolFormula>
A Herbrand interpretation is an interpretation for a first-order signature, stating all ground atoms that are true in the interpretation.
NOTE: We only allow Herbrand interpretations for signatures without function symbols.
Author:
Matthias Thimm
  • Constructor Details

    • HerbrandInterpretation

      public HerbrandInterpretation()
      Creates a new empty Herbrand interpretation.
    • HerbrandInterpretation

      public HerbrandInterpretation(Collection<? extends FolAtom> atoms)
      Creates a new Herbrand interpretation with the given set of atoms
      Parameters:
      atoms - the set of true atoms in this Herbrand interpretation.
  • Method Details

    • satisfies

      public boolean satisfies(FolFormula formula) throws IllegalArgumentException
      Checks whether this Herbrand interpretation satisfies the given formula.
      Parameters:
      formula - a formula.
      Returns:
      "true" if this interpretation satisfies "f".
      Throws:
      IllegalArgumentException - if "f" is not closed.
    • isSyntacticallyEquivalent

      public boolean isSyntacticallyEquivalent(HerbrandInterpretation other, Collection<? extends Collection<? extends Constant>> equivalenceClasses)
      Checks whether this interpretation is syntactically equivalent to the given interpretation and the given equivalence classes, i.e. whether this interpretation can be translated to the other one by substituting constants from the same equivalence classes
      Parameters:
      other - a Herbrand interpretation.
      equivalenceClasses - a set of sets of constants.
      Returns:
      "true" iff the two interpretations are syntactically equivalent.
    • satisfies

      public boolean satisfies(Set<FolFormula> formulas) throws IllegalArgumentException
      Checks whether this Herbrand interpretation satisfies each of the formulas in the given set of first-order formulas.
      Parameters:
      formulas - a set of first-order formulas.
      Returns:
      "true" if this interpretation satisfies the given set of formulas.
      Throws:
      IllegalArgumentException - if at least one formula does not correspond to the expected language.
    • satisfies

      public boolean satisfies(FolBeliefSet beliefBase) throws IllegalArgumentException
      Description copied from interface: Interpretation
      Checks whether this interpretation satisfies the given knowledge base.
      Parameters:
      beliefBase - a knowledge base.
      Returns:
      "true" if this interpretation satisfies the given knowledge base.
      Throws:
      IllegalArgumentException - IllegalArgumentException if the knowledgebase does not correspond to the expected language.
    • exchange

      public HerbrandInterpretation exchange(Term<?> t1, Term<?> t2)
      Substitutes every occurrence of "t1" by "t2" and vice versa and returns the new interpretation.
      Parameters:
      t1 - a term.
      t2 - a term.
      Returns:
      a Herbrand interpretation
    • exchange

      public HerbrandInterpretation exchange(Map<Term<?>,​Term<?>> mapping)
      For every mapping t1 -> t2, this method substitutes every occurrence of "t1" by "t2" and vice versa and returns the new interpretation
      Parameters:
      mapping - a mapping of terms.
      Returns:
      a Herbrand interpretation.
    • toString

      public String toString()
      Overrides:
      toString in class InterpretationSet<FolAtom,​FolBeliefSet,​FolFormula>