Class MlHerbrandBase


  • public class MlHerbrandBase
    extends java.lang.Object
    Modified version of HerbrandBase that allows for modal formulas. The Herbrand base is the set of all possible ground atoms of some given first-order logic.
    NOTE: We only allow to define a Herbrand base for signatures without function symbols.
    Author:
    Matthias Thimm, Anna Gessler
    See Also:
    HerbrandBase
    • Field Summary

      Fields 
      Modifier and Type Field Description
      private HerbrandBase hBase  
    • Constructor Summary

      Constructors 
      Constructor Description
      MlHerbrandBase​(FolSignature sig)
      Creates a new Herbrand base for the given signature.
    • Method Summary

      Modifier and Type Method Description
      java.util.Set<MlHerbrandInterpretation> getAllHerbrandInterpretations()
      Computes all possible Herbrand interpretations of this Herbrand base, i.e.
      java.util.Set<FolAtom> getAtoms()
      Returns all atoms of this Herbrand base.
      • Methods inherited from class java.lang.Object

        clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
    • Constructor Detail

      • MlHerbrandBase

        public MlHerbrandBase​(FolSignature sig)
                       throws java.lang.IllegalArgumentException
        Creates a new Herbrand base for the given signature.
        NOTE: We only allow to define a Herbrand base for signatures without function symbols.
        Parameters:
        sig - the underlying first-order signature for this Herbrand base. There should be no functors defined in "sig"
        Throws:
        java.lang.IllegalArgumentException - if "sig" contains a functor.
        See Also:
        HerbrandBase(FolSignature sig)
    • Method Detail

      • getAllHerbrandInterpretations

        public java.util.Set<MlHerbrandInterpretation> getAllHerbrandInterpretations()
        Computes all possible Herbrand interpretations of this Herbrand base, i.e. all possible subsets of this Herbrand base.
        Returns:
        all possible Herbrand interpretations of this Herbrand base, i.e. all possible subsets of this Herbrand base.
      • getAtoms

        public java.util.Set<FolAtom> getAtoms()
        Returns all atoms of this Herbrand base.
        Returns:
        all atoms of this Herbrand base.
        See Also:
        HerbrandBase.getAtoms()