All Packages  Class Hierarchy  This Package  Previous  Next  Index

Class JavaAgent.resource.fopl.Clause

java.lang.Object
   |
   +----JavaAgent.resource.fopl.Clause

public class Clause

extends Object

implements Parsable, KRSentence

See Also:

Literal

Clause()

This constructor is for the empty clause.

Clause(Literal)

This constructor for a Clause takes a single Literal as argument for this unit clause.

Clause(Vector)

This constructor for a Clause takes a Vector of Literals.

addLiteral(Literal)

This function adds a new Literal to this Clause.

addParamodulants(Literal, Clause, Literal, Vector)

This function adds certain paramodulants to the given Vector.

clone()

Cloning a Clause returns a new Clause consisting of clones of the Literals in the original Clause.

clone(Substitution)

Returns a copy of this Clause with Variables replaced according to the given Substitution.

disjoin(Clause)

This function adds the Literals (not clones) in the given Clause to this Clause.

equals(Object)

This function tests whether this and the given Object are equal.

getParents()

This function returns a Vector that contains all the direct parent Clauses to this Clause.

getParentSubstitution()

This function returns the Substitution that was used to derive this Clause.

getResolvent(Literal, Clause, Literal, Substitution)

This function generates a new Clause that is the resolvent of this Clause and the given Clause over the first given Literal in this Clause and the second given Literal in the given Clause where the given Substitution must be a unifying Substitution over these two Literals.

getResolvents(Literal, Clause, Vector)

This function generates all possible resolvents from this and the given Clause over the given Literal in this Clause and adds them to the given Vector.

getResolvents(Vector)

This function generates all possible resolvents from this and the given Vector of Clauses over one of this Clauses' Literals.

getVars()

This function returns the Variables in this Clause in a Vector.

hasAncestorClauses()

This funtion tests whether this Clause has an associated ancestry record of Clauses.

hasParent(KRSentence)

This function tests whether this Clause has the given Clause as a (direct) parent clause.

isEmpty()

This function test whether this Clause is the empty Cluase.

isTautology()

This function test whether this Clause is a tautology.

literals()

This function returns an Enumeration over the Literals in this Clause.

parse(InputStream)

This function can be used to parse a given InputStream that represents a Clause.

parse(String)

This function can be used to parse a given String that represents a Clause.

setParent(KRSentence, Substitution)

This function can be used to set the ancestor of this Clause to the given KRSentence.

testInequality(Vector, Literal)

This function tests whether the given Literal in this Clause is an inequality and adds a new derived Clause to the given Vector if possible.

toString()

A Clause is printed as ( <literal>* ).

 public Clause()

This constructor is for the empty clause.

 public Clause(Literal aLit) throws IllegalArgumentException

This constructor for a Clause takes a single Literal as argument for this unit clause.

Parameters:

aLit - the Literal in this Clause

Throws: IllegalArgumentException

An exception will occur if the given Literal is null. In this case the constructor for an empty Clause (above) should be used.

 public Clause(Vector someLits) throws IllegalArgumentException

This constructor for a Clause takes a Vector of Literals. All elements of the Vector must be Literals! Literals occuring twice in the Vector will only be added once.

Parameters:

someLits - the Vector of Literals in this Clause

Throws: IllegalArgumentException

An exception will occur if the given Vector is null or one of its elements is not a Literal.

 public Object clone()

Cloning a Clause returns a new Clause consisting of clones of the Literals in the original Clause. The new Clause comes with the same Variables as the original.

Returns:

a new Clause with equal Literals

Overrides:

clone in class Object

 public Clause clone(Substitution s) throws IllegalArgumentException

Returns a copy of this Clause with Variables replaced according to the given Substitution. Symbols in the copy will be the same as the original ones but Variables will be repalced by the respective Terms in the given 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. If two of the Literals become equal in this process only one will occur in the result.

This function can also be used to generate a copy of this Formula that contains a new set of Variables. The given Substitution should be a new, empty Substitution in this case. Otherwise cloning can be seen as instantiating the Clause.

Parameters:

s - the Substitution that tells us how to replace Variables

Returns:

a new Clause that is an instance of this Clause; the Substitution s will be 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.

 public Vector getVars()

This function returns the Variables in this Clause in a Vector. No Variable is in the Vector twice though, i.e. it is like a set of Variables.

Returns:

a Vector of Variables in this Clause

 public boolean isEmpty()

This function test whether this Clause is the empty Cluase.

Returns:

true iff this clause contains no Literals

 public boolean isTautology()

This function test whether this Clause is a tautology. This will be true if it contains two complementary Literal.

Returns:

true iff this clause is a tautology

 public void addLiteral(Literal aLit) throws IllegalArgumentException

This function adds a new Literal to this Clause. If it is already in the Clause or is an inequality between two equal Terms it won't be added. This function uses the equals() test to determine this.

Parameters:

aLit - the new Literal to be appended

Throws: IllegalArgumentException

An exception will occur if the given Literal is null.

 public void disjoin(Clause c) throws IllegalArgumentException

This function adds the Literals (not clones) in the given Clause to this Clause. Duplicates are eliminated.

Parameters:

c - the Clause to be appended

Throws: IllegalArgumentException

An exception will occur if the given Clause is null.

 public Vector getResolvents(Vector clauses) throws IllegalArgumentException

This function generates all possible resolvents from this and the given Vector of Clauses over one of this Clauses' Literals. For this purpose it will first generate all resolvents over all Literals in this Clause. It will then select the Literal which generated the smallest number of resolvents and return the resolvents of this Literal.

Parameters:

a - Vector of Clauses this one is to be resolved with

Returns:

a Vector of Clauses which are all possible resolvents over only one of the Literals in this Clause and all given Clauses with complementary Literals

Throws: IllegalArgumentException

An exception will occur if the given Vector is null.

 protected void testInequality(Vector resolvents,
                               Literal lit)

This function tests whether the given Literal in this Clause is an inequality and adds a new derived Clause to the given Vector if possible. The added Clause is basically the result of a resolution step with the Literal (= ?x ?x).

Parameters:

resolvents - the Vector to which the result may be added

lit - a Literal in this Clause

 protected void getResolvents(Literal lit,
                              Clause other,
                              Vector res) throws IllegalArgumentException

This function generates all possible resolvents from this and the given Clause over the given Literal in this Clause and adds them to the given Vector.

Parameters:

lit - a Literal in this Clause

other - the Clause this one is to be resolved with

res - A Vector of Clauses; new resolvents generated here will be added to this Vector

Throws: IllegalArgumentException

An exception will occur if the given Clause or the given Vector are null

 protected Clause getResolvent(Literal myLit,
                               Clause otherCl,
                               Literal otherLit,
                               Substitution s) throws IllegalArgumentException

This function generates a new Clause that is the resolvent of this Clause and the given Clause over the first given Literal in this Clause and the second given Literal in the given Clause where the given Substitution must be a unifying Substitution over these two Literals. The resolvent Clause will contain a new set of Variables and no duplicate Literals will be in this Clause.

If the two Literals are not members of the respective Clauses or if they are not complementary under the given Substitution then the behaviour of this function is undefined. It may cause exceptions or just generate a meaningless Clause.

Parameters:

myLit - a Literal in this Clause

otherCl - the second Clause that will be used to generate the resolvent

otherLit - a Literal in otherCl that must be complementary to myLit

s - a unifying Substitution for myLit and otherLit

Returns:

a new Clause that is the resolvent of this and the given Clause over the given Literals; the given Substitution will be extended to keep track of Variable mappings

Throws: IllegalArgumentException

An exception may occur if the given Clause or Substitution are null.

 protected void addParamodulants(Literal lit,
                                 Clause other,
                                 Literal eqLit,
                                 Vector res)

This function adds certain paramodulants to the given Vector. Only FunctTerms in the first given Literal which must be in this Clause will be replaced. Replacements are determined solely by the given Literal which should be an equality in the other Clause.

Parameters:

lit - a Literal in this Clause

other - another Clause

eqLit - an equality in the other Clause

res - the Vector new Clauses are to be added to

 protected void setParent(KRSentence krs,
                          Substitution s)

This function can be used to set the ancestor of this Clause to the given KRSentence.

Parameters:

krs - the parent KRSentence

 protected boolean hasParent(KRSentence cl)

This function tests whether this Clause has the given Clause as a (direct) parent clause.

Parameters:

cl - the potential parent Clause

Returns:

true iff the given Clause is a parent of this Clause

 protected Vector getParents()

This function returns a Vector that contains all the direct parent Clauses to this Clause. It returns null if no parents are known.

Returns:

a Vector that contains all the direct parent Clauses to this Clause

 protected Substitution getParentSubstitution()

This function returns the Substitution that was used to derive this Clause. It returns null if no parents are known.

Returns:

the Substitution that was used to derive this Clause

 protected boolean hasAncestorClauses()

This funtion tests whether this Clause has an associated ancestry record of Clauses.

Returns:

true iff the are known ancestors to this Clause

 public Enumeration literals()

This function returns an Enumeration over the Literals in this Clause.

Returns:

an Enumeration over the Literals in this Clause

 public String toString()

A Clause is printed as ( <literal>* ).

Returns:

the String that represents this Clause

Overrides:

toString in class Object

 public boolean equals(Object otherCl)

This function tests whether this and the given Object are equal. In general, two Clauses are equal if they contain equal Literals in the same order. This is not a test for logical equivalence or unifyability!

Parameters:

otherForm - the Clause this one is to be compared to

Returns:

whether the given Object is equal to this one

Overrides:

equals in class Object

 public static Clause parse(String s) throws IllegalArgumentException, ParseException

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

 <clause>    ::= ( <signedlit>* )
 <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 Clause parse(InputStream ist) throws IllegalArgumentException, IOException, ParseException

This function can be used to parse a given InputStream that represents a Clause. The syntax in BNF is as above except that the first token should be the word CLAUSE 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