    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

A Clause is a set of Literals (or Propositions). Implicitely, the Literals in a Clause are disjunctively connected.

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>* ).

##

Clause

     public Clause()

  This constructor is for the empty clause.

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.

Clause

     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.

##

clone

     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

clone

     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.

getVars

     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

isEmpty

     public boolean isEmpty()

  This function test whether this Clause is the empty Cluase.

  Returns:
    `true` iff this clause contains no Literals

isTautology

     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

addLiteral

     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.

disjoin

     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.

getResolvents

     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.

testInequality

     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

getResolvents

     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

getResolvent

     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.

addParamodulants

     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

setParent

     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

hasParent

     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

getParents

     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

getParentSubstitution

     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

hasAncestorClauses

     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

literals

     public Enumeration literals()

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

  Returns:
    an Enumeration over the Literals in this Clause

toString

     public String toString()

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

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

equals

     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

parse

     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.

parse

     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