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

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.

 protected boolean negated

This variable indicates whether this Literal is negated.

 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.

 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.

 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.

 protected Literal()

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

 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

 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

 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.

 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.

 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

 public boolean isPositive()

This function tests whether this is a positive Literal.

Returns:

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

 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 "="

 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.

 public void negate()

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

 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.

 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.

 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

 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.

 public Enumeration arguments()

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

Returns:

an Enumeration over the arguments of this Literal

 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

 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

 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

 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.

 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