Package org.tweetyproject.logics.fol.syntax

Class FolAtom

java.lang.Object
org.tweetyproject.logics.commons.syntax.RelationalFormula
org.tweetyproject.logics.fol.syntax.FolFormula
org.tweetyproject.logics.fol.syntax.FolAtom
All Implemented Interfaces:
Formula, Atom, ClassicalFormula, ComplexLogicalFormula, Conjunctable, Disjunctable, Invertable, LogicStructure, ProbabilityAware, QuantifiedFormula, SimpleLogicalFormula
public class FolAtom extends FolFormula implements Atom
An atom in first-order logic, i.e. a predicate and a list of argument terms.
Author:
Matthias Thimm

  • Constructor Details

    • FolAtom

      public FolAtom()
      Default-Ctor: Creates new empty FOL-Atom

    • FolAtom

      public FolAtom(Predicate predicate)
      Creates a new atom with the given predicate and initializes an empty argument list.
      Parameters:
      predicate - the predicate of the atom.

    • FolAtom

      public FolAtom(Predicate predicate, Term<?>... terms)
      constructs FolAtom
      Parameters:
      predicate - predicate
      terms - terms

    • FolAtom

      public FolAtom(Predicate predicate, List<? extends Term<?>> arguments)
      Creates a new atom with the given predicate and list of terms
      Parameters:
      predicate - the predicate of the atom
      arguments - the arguments (terms) of the atom

    • FolAtom

      public FolAtom(FolAtom other)
      Parameters:
      other - another Atom

  • Method Details

    • addArgument

      public void addArgument(Term<?> term) throws IllegalArgumentException
      Appends the given argument to this atom's arguments and returns itself.
      Specified by:
      addArgument in interface Atom
      Parameters:
      term - an argument to be added
      Throws:
      IllegalArgumentException - if the given term does not correspond to the expected sort or the argument list is complete.

    • substitute

      public FolAtom substitute(Term<?> v, Term<?> t) throws IllegalArgumentException
      Description copied from class: RelationalFormula
      Substitutes all occurrences of term "v" in this formula by term "t" and returns the new formula. NOTE: if "v" is a variable and bound to a quantifier then "v" is not substituted in that quantifiers inner formula.
      Specified by:
      substitute in interface ComplexLogicalFormula
      Specified by:
      substitute in class FolFormula
      Parameters:
      v - the term to be substituted.
      t - the term to substitute.
      Returns:
      a formula where every occurrence of "v" is replaced by "t".
      Throws:
      IllegalArgumentException - if "v" and "t" are of different sorts (NOTE: this exception is only thrown when "v" actually appears in this formula).

    • getAtoms

      public Set<FolAtom> getAtoms()
      Description copied from interface: SimpleLogicalFormula
      Processes the set of all atoms which appear in this formula
      Specified by:
      getAtoms in interface SimpleLogicalFormula
      Specified by:
      getAtoms in class RelationalFormula
      Returns:
      all atoms that appear in this formula.

    • isComplete

      public boolean isComplete()
      Checks whether this atom is complete, i.e. whether every argument is set.
      Specified by:
      isComplete in interface Atom
      Returns:
      "true" if the atom is complete.

    • getUnboundVariables

      public Set<Variable> getUnboundVariables()
      Specified by:
      getUnboundVariables in interface QuantifiedFormula
      Returns:
      a set of of unbound variables

    • getPredicates

      public Set<Predicate> getPredicates()
      Description copied from interface: SimpleLogicalFormula
      Processes the set of all predicates which appear in this formula
      Specified by:
      getPredicates in interface SimpleLogicalFormula
      Returns:
      all predicates that appear in this formula

    • getFunctors

      public Set<Functor> getFunctors()
      Specified by:
      getFunctors in class RelationalFormula
      Returns:
      all functors that appear in this formula.

    • isClosed

      public boolean isClosed()
      Description copied from interface: QuantifiedFormula
      Checks whether this formula is closed, i.e. whether every variables occurring in the formula is bound by a quantifier.
      Specified by:
      isClosed in interface QuantifiedFormula
      Returns:
      "true" if this formula is closed, "false" otherwise.

    • isClosed

      public boolean isClosed(Set<Variable> boundVariables)
      Description copied from interface: QuantifiedFormula
      Checks whether this formula is closed, i.e. whether every variables occurring in the formula is bound by a quantifier. Every variable in "boundVariables" is already assumed to be bound.
      Specified by:
      isClosed in interface QuantifiedFormula
      Parameters:
      boundVariables - the variables assumed to be bound.
      Returns:
      "true" if this formula is closed wrt. "boundVariables", "false" otherwise.

    • isWellBound

      public boolean isWellBound()
      Description copied from interface: QuantifiedFormula
      Checks whether this formula is well-bound, i.e. whether no variable bound by a quantifier is again bound by another quantifier within the first quantifier's range.
      Specified by:
      isWellBound in interface QuantifiedFormula
      Returns:
      "true" if this formula is well-bound, "false" otherwise.

    • isWellBound

      public boolean isWellBound(Set<Variable> boundVariables)
      Description copied from interface: QuantifiedFormula
      Checks whether this formula is well-bound, i.e. whether no variable bound by a quantifier is again bound by another quantifier within the first quantifier range. Every variable in "boundVariables" is assumed to be bound already.
      Specified by:
      isWellBound in interface QuantifiedFormula
      Parameters:
      boundVariables - the variables assumed to be bound.
      Returns:
      "true" if this formula is well-bound, "false" otherwise.

    • containsQuantifier

      public boolean containsQuantifier()
      Description copied from interface: QuantifiedFormula
      Checks whether this formula contains any quantification.
      Specified by:
      containsQuantifier in interface QuantifiedFormula
      Returns:
      "true" if this formula contains a quantification.

    • getPredicate

      public Predicate getPredicate()
      Returns the predicate of this atom
      Specified by:
      getPredicate in interface Atom
      Returns:
      the predicate of this atom

    • getArguments

      public List<Term<?>> getArguments()
      Specified by:
      getArguments in interface Atom
      Returns:
      the arguments of this atom.

    • isDnf

      public boolean isDnf()
      Description copied from class: FolFormula
      Checks whether this formula is in disjunctive normal form.
      Specified by:
      isDnf in class FolFormula
      Returns:
      "true" iff this formula is in disjunctive normal form.

    • isLiteral

      public boolean isLiteral()
      Specified by:
      isLiteral in interface SimpleLogicalFormula
      Returns:
      true if the formula represents a literal in the language or false otherwise

    • toString

      public String toString()
      Specified by:
      toString in class RelationalFormula

    • toNnf

      public FolFormula toNnf()
      Description copied from class: FolFormula
      Makes the negation normal form of this formula.
      Specified by:
      toNnf in class FolFormula
      Returns:
      the NNF of this formula

    • collapseAssociativeFormulas

      public FolFormula collapseAssociativeFormulas()
      Description copied from class: FolFormula
      This method collapses all associative operations appearing in this term, e.g. every a||(b||c) becomes a||b||c.
      Specified by:
      collapseAssociativeFormulas in class FolFormula
      Returns:
      the collapsed formula.

    • hashCode

      public int hashCode()
      Specified by:
      hashCode in interface SimpleLogicalFormula
      Overrides:
      hashCode in class Object

    • equals

      public boolean equals(Object obj)
      Specified by:
      equals in interface SimpleLogicalFormula
      Overrides:
      equals in class Object

    • getTerms

      public Set<Term<?>> getTerms()
      Specified by:
      getTerms in interface LogicStructure
      Returns:
      a set containing all terms of this logical structure

    • getTerms

      public <C extends Term<?>> Set<C> getTerms(Class<C> cls)
      Description copied from interface: LogicStructure
      Processes the set containing all terms of type C. This method uses the equals method of the given Class and therefore does not add terms which are sub classes of type C to the set.
      Specified by:
      getTerms in interface LogicStructure
      Type Parameters:
      C - the type of terms
      Parameters:
      cls - The Class structure containing type information about the searched term
      Returns:
      A set containing all terms of type C of this logical structure

    • clone

      public FolAtom clone()
      Description copied from interface: SimpleLogicalFormula
      Creates a deep copy of this formula
      Specified by:
      clone in interface ComplexLogicalFormula
      Specified by:
      clone in interface SimpleLogicalFormula
      Specified by:
      clone in class FolFormula
      Returns:
      the cloned formula

    • setPredicate

      public Atom.RETURN_SET_PREDICATE setPredicate(Predicate newer)
      Description copied from interface: Atom
      Changes the predicate of the atom. Given an old Predicate po and a new predicate pn with their list of arguments types at(po) and at(pn) and the arguments of this Atom: arg(this) this method distinguishes between three cases: 1. The predicate only differ in the names, returning RSP_SUCCESS 2. The old predicates argument types is a sub-list of the new argument types then the method returns RSP_INCOMPLETE and the atoms isComplete() method returns false 3. The new predicates argument types is a sub-list of the old argument types then the method returns RSP_TRUNCATED and the arguments of this atom are truncated too and isComplete() returns true. 4. The old and new predicates' argument types differ then the list of arguments of the atom get cleared and isComplete() returns false.
      Specified by:
      setPredicate in interface Atom
      Parameters:
      newer - some predicate
      Returns:
      Depends on the cases described above: 1. RSP_SUCCESS 2. RSP_INCOMPLETE 3. RSP_TRUNCATED 4. RSP_CLEARED

    • getName

      public String getName()
      Specified by:
      getName in interface Atom
      Returns:
      the name of the predicate