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
    • Field Summary

      Fields 
      Modifier and Type Field Description
      private java.util.Set<FolAtom> atoms
      The atoms of this Herbrand base.
    • 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.
      private java.util.Set<FolAtom> getAllInstantiations​(FolSignature sig, Predicate p, java.util.List<Term<?>> arguments)
      Computes all instantiations of the predicate "p" relative to the signature "sig" where "arguments" defines the first arguments of the atoms.
      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
    • Field Detail

      • atoms

        private java.util.Set<FolAtom> atoms
        The atoms of this Herbrand base.
    • 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

      • getAllInstantiations

        private java.util.Set<FolAtom> getAllInstantiations​(FolSignature sig,
                                                            Predicate p,
                                                            java.util.List<Term<?>> arguments)
        Computes all instantiations of the predicate "p" relative to the signature "sig" where "arguments" defines the first arguments of the atoms.
        Parameters:
        sig - a signature for which the instantiations should be computed.
        p - the predicate of the atoms.
        arguments - the currently set arguments of the atoms.
        Returns:
        the complete set of instantiations of "p" relative to "sig" and "arguments".
      • 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.