Class MlHerbrandInterpretation
java.lang.Object
org.tweetyproject.commons.AbstractInterpretation<B,S>
org.tweetyproject.commons.InterpretationSet<FolAtom,FolBeliefSet,FolFormula>
org.tweetyproject.logics.ml.semantics.MlHerbrandInterpretation
- All Implemented Interfaces:
Iterable<FolAtom>
,Collection<FolAtom>
,Interpretation<FolBeliefSet,
FolFormula>
Modified version of HerbrandInterpretation that allows for modal formulas.
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.
NOTE: We only allow Herbrand interpretations for signatures without function symbols.
- Author:
- Matthias Thimm, Anna Gessler
- See Also:
-
Constructor Summary
ConstructorDescriptionCreates a new empty Herbrand interpretationMlHerbrandInterpretation
(Collection<? extends FolAtom> atoms) Creates a new Herbrand interpretation with the given set of atoms -
Method Summary
Modifier and TypeMethodDescriptionFor every mapping t1 -> t2, this method substitutes every occurrence of "t1" by "t2" and vice versa and returns the new interpretationSubstitutes every occurrence of "t1" by "t2" and vice versa and returns the new interpretation.boolean
isSyntacticallyEquivalent
(MlHerbrandInterpretation 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.boolean
satisfies
(Set<FolFormula> formulas) Checks whether this Herbrand interpretation satisfies each of the formulas in the given set of first-order formulas.boolean
satisfies
(Formula formula, Set<Interpretation<FolBeliefSet, FolFormula>> successors) Checks whether this Herbrand interpretation satisfies the given formula.boolean
satisfies
(FolBeliefSet beliefBase) Checks whether this interpretation satisfies the given knowledge base.boolean
satisfies
(FolFormula formula) Checks whether this interpretation satisfies the given formula.toString()
Methods inherited from class org.tweetyproject.commons.InterpretationSet
add, add, addAll, clear, contains, containsAll, equals, hashCode, isEmpty, iterator, remove, removeAll, retainAll, size, toArray, toArray
Methods inherited from class org.tweetyproject.commons.AbstractInterpretation
satisfies
Methods inherited from interface java.util.Collection
parallelStream, removeIf, spliterator, stream, toArray
-
Constructor Details
-
MlHerbrandInterpretation
public MlHerbrandInterpretation()Creates a new empty Herbrand interpretation -
MlHerbrandInterpretation
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
Description copied from interface:Interpretation
Checks whether this interpretation satisfies the given formula.- Parameters:
formula
- a formula .- Returns:
- "true" if this interpretation satisfies the given formula.
- Throws:
IllegalArgumentException
- if the formula does not correspond to the expected language.
-
satisfies
public boolean satisfies(Formula formula, Set<Interpretation<FolBeliefSet, FolFormula>> successors) throws IllegalArgumentExceptionChecks whether this Herbrand interpretation satisfies the given formula.- Parameters:
formula
- a formula.successors
- the successors- Returns:
- "true" if this interpretation satisfies "f".
- Throws:
IllegalArgumentException
- if "f" is not closed.
-
isSyntacticallyEquivalent
public boolean isSyntacticallyEquivalent(MlHerbrandInterpretation 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
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
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
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
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
- Overrides:
toString
in classInterpretationSet<FolAtom,
FolBeliefSet, FolFormula>
-