Class HerbrandBase


  • public class HerbrandBase
    extends java.lang.Object
    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
    • Constructor Summary

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

      Modifier and Type Method Description
      java.util.Set<HerbrandInterpretation> 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

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

      • HerbrandBase

        public HerbrandBase​(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.
    • Method Detail

      • getAllHerbrandInterpretations

        public java.util.Set<HerbrandInterpretation> 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.