    All Packages  Class Hierarchy  This Package  Previous  Next  Index

# Class JavaAgent.resource.fopl.Literal

    java.lang.Object
       |
       +----JavaAgent.resource.fopl.Formula
               |
               +----JavaAgent.resource.fopl.Literal

public class Literal
extends Formula
implements Parsable

A Literal is one of the most basic building blocks for a Formula. It consists of a predicate symbol followed by one or more arguments which must be Terms. The predicate represents a relation between the arguments. A Literal may also have a sign which indicates whether it is negated or not.

See Also:
  Proposition, Term

##

negated
  This variable indicates whether this Literal is negated.
theTerms
  This Vector of Terms contains the predicate and the agument Terms in this Literal.

##

Literal()
  This protected constructor creates an empty Literal.
Literal(boolean, Symbol, Term, Term)
  This protected constructor for a Literal takes a boolean indecating whether the Literal is negated, a Symbol (the predicate) and two Terms which are the two arguments.
Literal(Symbol, Vector)
  This constructor for a Literal takes a Symbol and a list of arguments.

##

allSubTerms()
  This function returns an Enumeration over all sub-terms in this Literal.
arguments()
  This function returns an Enumeration over the arguments of this Literal.
clone()
  Cloning a Literal returns a new Literal consisting of the same predicate symbol and a clone of each argument.
clone(Substitution)
  Cloning a Literal returns a new Literal consisting of the same predicate symbol and a clone of each argument with the given Substitution.
clone(Substitution, Term, Term)
  Cloning a Literal returns a new Literal consisting of the same predicate symbol and a clone of each argument with the given Substitution but with the first given sub-Term replaced by the second given Term.
complements(Literal)
  This function tests whether this and the given Literal completmentary.
complements(Literal, Substitution)
  This function attempts to extend the given Substitution so that this Literal and the given Literal are complementary.
equals(Object)
  This function tests whether this and the given Object are equal.
getVars(Vector)
  This function adds the Variables in this Literal to the given Vector.
isEquality()
  This function tests whether this Literal represents an equality or inequality.
isPositive()
  This function tests whether this is a positive Literal.
negate()
  This function can be used to change the sign of this Literal.
nthArgument(int)
  This function returns the n-th argument to this Literal.
parseLit(InputStream)
  This function can be used to parse a given InputStream that represents a Literal.
parseLit(String)
  This function can be used to parse a given String that represents a Literal.
signedUnify(Literal, Substitution)
  This function attempts to extend the given Substitution so that this Literal and the given Literal are unified.
toSkolemizedAndOrForm(Substitution, Vector, boolean)
  This function returns a new Literal which is a copy of this Literal.
toString()
  A Literal is printed as ( <constant> <term>+ ) or (NOT ( <constant> <term>+ )) if it was negated.
unify(Literal, Substitution)
  This function attempts to extend the given Substitution so that this Literal and the given Literal are unified.

##

negated

     protected boolean negated

  This variable indicates whether this Literal is negated.

theTerms

     protected Vector theTerms

  This Vector of Terms contains the predicate and the agument Terms in this Literal. The first Term should be a ConstTerm containing the Symbol that represents the predicate.

##

Literal

     public Literal(Symbol aSy,
                    Vector someTerms) throws IllegalArgumentException

  This constructor for a Literal takes a Symbol and a list of arguments. All elements of the given Vector must be Terms!

  Parameters:
    aSy - the predicate Symbol
    someTerms - the Vector of argument Terms
  Throws: IllegalArgumentException
    An exception will occur if the given Symbol is null, the given Vector is null or empty, or one of the elements of the Vector is not a Term.

Literal

     public Literal(boolean neg,
                    Symbol aSy,
                    Term t1,
                    Term t2) throws IllegalArgumentException

  This protected constructor for a Literal takes a boolean indecating whether the Literal is negated, a Symbol (the predicate) and two Terms which are the two arguments.

  Parameters:
    neg - the sign of this Literal
    aSy - the predicate Symbol
    t1 - the first argument Term
    t2 - the second argument Term
  Throws: IllegalArgumentException
    An exception will occur if the given Symbol or one of the given Terms is null.

Literal

     protected Literal()

  This protected constructor creates an empty Literal. The Vector must be filled before anything else should be done with the Literal.

##

clone

     public Object clone()

  Cloning a Literal returns a new Literal consisting of the same predicate symbol and a clone of each argument. Symbols and Variables in the copy will be the same as in the original.

  Returns:
    an equal copy of this Literal
  Overrides:
    clone in class Formula

clone

     public Formula clone(Substitution s)

  Cloning a Literal returns a new Literal consisting of the same predicate symbol and a clone of each argument with the given Substitution. That is, Variables occuring in the argument Terms will be replaced by Terms they are mapped to in the Substitution. A Variable not occurring in the Substitution will be replaced by a new (different) Variable with the same name. The given Substitution will be extended to include the mappings of old Variables to new ones.

  Parameters:
    s - the Substitution that tells us how to replace Variables
  Returns:
    a new Literal that is an instance of this Literal; the Substitution `s` will extended with any new Variable replacements introduced
  Throws: IllegalArgumentException
    An exception can occur if the given Substitution is null. In this case `clone()` (above) should be used.
  Overrides:
    clone in class Formula

clone

     protected Literal clone(Substitution s,
                             Term t,
                             Term rTerm)

  Cloning a Literal returns a new Literal consisting of the same predicate symbol and a clone of each argument with the given Substitution but with the first given sub-Term replaced by the second given Term. Apart from the Term replacement this function is just like `clone(Substitution)` above.

  Parameters:
    s - the Substitution that tells us how to replace Variables
    t - the sub-Term in this Literal to be replaced
    rTerm - the (uninstantiated) replacement Term
  Returns:
    a new Literal that is, apart from the replaced Term, an instance of this Literal; the Substitution `s` will extended with any new Variable replacements introduced
  Throws: IllegalArgumentException
    An exception can occur if the given Substitution or either of the given Terms is null.

getVars

     public void getVars(Vector vars) throws IllegalArgumentException

  This function adds the Variables in this Literal to the given Vector. No Variable is added twice though.

  Parameters:
    vars - a Vector of Variables that will be extended
  Throws: IllegalArgumentException
    An exception can occur if the given Vector is null.

toSkolemizedAndOrForm

     protected Formula toSkolemizedAndOrForm(Substitution s,
                                             Vector allQuantVars,
                                             boolean isNegated)

  This function returns a new Literal which is a copy of this Literal. The given Substitution and the given Vector of Variables will be ignored here. Finally, the given boolean indicates whether the Literal is to be negated, i.e. its sign to be reversed.

  Parameters:
    s - a Substitution (will be ignored)
    allQuantVars - the Vector of universally quantified Variables (will be ignored)
    isNegated - whether the Literal has to be negated
  Returns:
    a new Literal with the given boolean worked into the sign
  Overrides:
    toSkolemizedAndOrForm in class Formula

isPositive

     public boolean isPositive()

  This function tests whether this is a positive Literal.

  Returns:
    whether this Literal is positive, i.e. not negated

isEquality

     public boolean isEquality()

  This function tests whether this Literal represents an equality or inequality. Use `isPositive()` above to find out which one it is.

  Returns:
    whether the predicate in this Literal is "="

nthArgument

     public Term nthArgument(int n) throws ArrayIndexOutOfBoundsException

  This function returns the n-th argument to this Literal. The first argument has the index 1.

  Parameters:
    n - the index of the argument Term to be retrieved
  Returns:
    the n-th argument
  Throws: ArrayIndexOutOfBoundsException
    An exception will occur if the given index specifies a not existing argument.

negate

     public void negate()

  This function can be used to change the sign of this Literal.

unify

     public boolean unify(Literal other,
                          Substitution s) throws IllegalArgumentException, UnificationException

  This function attempts to extend the given Substitution so that this Literal and the given Literal are unified. It returns `true` if and only if this is possible. The sign of the two Literals is ignored for this purpose.

  Parameters:
    other - the other Literal this Literal is to be unified with
    s - the Substitution to be extended for the unification
  Returns:
    whether a unifying extension of the given Substitution was possible
  Throws: IllegalArgumentException
    An exception will occur if the given Literal or the given Substitution are null.
  Throws: UnificationException
    An exception can occur if the given Substitution was already finshed.

signedUnify

     public boolean signedUnify(Literal other,
                                Substitution s) throws IllegalArgumentException, UnificationException

  This function attempts to extend the given Substitution so that this Literal and the given Literal are unified. It returns `true` if and only if this is possible. The sign of the two Literals must be identical for this purpose.

  Parameters:
    other - the other Literal this Literal is to be unified with
    s - the Substitution to be extended for the unification
  Returns:
    whether a unifying extension of the given Substitution was possible
  Throws: IllegalArgumentException
    An exception will occur if the given Literal or the given Substitution are null.
  Throws: UnificationException
    An exception can occur if the given Substitution was already finshed.

complements

     public boolean complements(Literal otherLit)

  This function tests whether this and the given Literal completmentary. This will be the case if they have the same predicte and all the argument Terms are equal, but the signs are different.

  Parameters:
    otherLit - the Literal this one is to be compared to
  Returns:
    whether the given Literal is complemetary to this one

complements

     public boolean complements(Literal other,
                                Substitution s) throws IllegalArgumentException, UnificationException

  This function attempts to extend the given Substitution so that this Literal and the given Literal are complementary. It returns `true` if and only if this is possible. The sign of the two Literals must be different for this purpose.

  Parameters:
    other - the other Literal this Literal is to be unified with
    s - the Substitution to be extended for the unification
  Returns:
    whether a unifying extension of the given Substitution was possible and the two signs are complementary
  Throws: IllegalArgumentException
    An exception will occur if the given Literal or the given Substitution are null.
  Throws: UnificationException
    An exception can occur if the given Substitution was already finshed.

arguments

     public Enumeration arguments()

  This function returns an Enumeration over the arguments of this Literal.

  Returns:
    an Enumeration over the arguments of this Literal

allSubTerms

     public Enumeration allSubTerms()

  This function returns an Enumeration over all sub-terms in this Literal. Note that this is not an Enumeration over the arguments but every sub-Term within this Literal.

  Returns:
    an Enumeration over all sub-Terms in this Literal

toString

     public String toString()

  A Literal is printed as ( <constant> <term>+ ) or (NOT ( <constant> <term>+ )) if it was negated.

  Returns:
    the String that represents this Literal
  Overrides:
    toString in class Object

equals

     public boolean equals(Object otherForm)

  This function tests whether this and the given Object are equal. In general, two Literals are equal if they have the same sign, predicte, and all the argument Terms are equal.

  Parameters:
    otherForm - the Formula this one is to be compared to
  Returns:
    whether the given Object is equal to this one
  Overrides:
    equals in class Formula

parseLit

     public static Literal parseLit(String s) throws IllegalArgumentException, ParseException

  This function can be used to parse a given String that represents a Literal. The syntax in BNF is as follows:

       <signedlit> ::= <literal> | ( not <literal> )
       <literal>    ::= <constant> |
                        ( = <term> <term> )
                        ( <constant> <term>+ )
       <term>       ::= <constant> | <variable> |
                        ( <constant> <term>+ ) |
       <variable>   ::= ?<name>
       <constant>   ::= <name>

  Throws: IllegalArgumentException
    An exception will occur if the supplied String is empty or null.
  Throws: ParseException
    An exception can occur if parsing failed. Potential reasons include a syntax error or an I/O problem.

parseLit

     public static Literal parseLit(InputStream ist) throws IllegalArgumentException, IOException, ParseException

  This function can be used to parse a given InputStream that represents a Literal. The syntax in BNF is as above except that the first token should be the word `LITERAL` so that the generic parser knows what it has to expect. This is added automatically when parsing a String.

  Throws: IllegalArgumentException
    An exception will occur if the supplied InputStream is null.
  Throws: IOException
    An exception can occur if there are problems reading from the given InputStream.
  Throws: ParseException
    An exception can occur if parsing failed. Potential reasons include a syntax error.

    All Packages  Class Hierarchy  This Package  Previous  Next  Index