    All Packages  Class Hierarchy  This Package  Previous  Next  Index

# Class JavaAgent.resource.fopl.ClauseSet

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

public class ClauseSet
extends Object
implements Parsable, KnowledgeBase

A ClauseSet is a set of Clauses. ClauseSets can be constructed from a Formula or a FormulaSet and then tested for inconsistency. They will construct a resolution theorem prover to do so.

See Also:
  Clause, RTProver

##

ClauseSet()
  This constructor creates an empty ClauseSet.
ClauseSet(Clause)
  This constructor for a ClauseSet takes a single Clause as its argument.
ClauseSet(Formula)
  This constructor creates a ClauseSet that contains the Skolemized clause form version of the given Formula.
ClauseSet(FormulaSet)
  This constructor creates a ClauseSet that contains the Skolemized clause form version of the given Formulae in the given FormulaSet.

##

assert(ClauseSet)
  This function can be used to add knowledge to this KnowledgeBase.
assert(KRSentence)
  This function can be used to add knowledge to this KnowledgeBase.
clone()
  Cloning a ClauseSet returns a new ClauseSet consisting of clones of the Clauses in the original ClauseSet.
evaluate(KRSentence)
  This function takes a Clause and evaluates it against this ClauseSet.
isInconsistent()
  This function tests whether this KnowledgeBase is inconsistent.
parse(InputStream)
  This function can be used to parse a given InputStream that represents a ClauseSet.
sentences()
  This function returns an Enumerator for the Clauses in this ClauseSet.
setTraceStream(OutputStream)
  This function can be used create a trace of the functions `isInconsistent()` and `evaluate()`.
writeToStream(OutputStream)
  This function writes the content of this KnowledgeBase to the given OutputStream.

##

ClauseSet

     public ClauseSet()

  This constructor creates an empty ClauseSet.

ClauseSet

     public ClauseSet(Clause aCl) throws IllegalArgumentException

  This constructor for a ClauseSet takes a single Clause as its argument.

  Parameters:
    aCl - the single Clause this set will contain initially
  Throws: IllegalArgumentException
    An exception will occur if the given Clause is null. In this case the constructor for an empty ClauseSet (above) should be used.

ClauseSet

     public ClauseSet(Formula aForm) throws IllegalArgumentException

  This constructor creates a ClauseSet that contains the Skolemized clause form version of the given Formula.

  Parameters:
    aForm - the Formula for which the Clauses are to be created
  Throws: IllegalArgumentException
    An exception will occur if the given Formula is null.

ClauseSet

     public ClauseSet(FormulaSet forms) throws IllegalArgumentException

  This constructor creates a ClauseSet that contains the Skolemized clause form version of the given Formulae in the given FormulaSet.

  Parameters:
    forms - the FormulaSet for which the Clauses are to be created
  Throws: IllegalArgumentException
    An exception will occur if the given FormulaSet is null.

##

clone

     public Object clone()

  Cloning a ClauseSet returns a new ClauseSet consisting of clones of the Clauses in the original ClauseSet.

  Returns:
    a copy of this ClauseSet
  Overrides:
    clone in class Object

assert

     public void assert(KRSentence sent) throws IllegalArgumentException, FormalismException

  This function can be used to add knowledge to this KnowledgeBase. The asserted KRSentence must be a Clause.

  Parameters:
    sent - the Clause holding the new knowledge
  Throws: IllegalArgumentException
    An exception will occur if the given KRSentence is null.
  Throws: FormalismException
    An exception will occur if the given KRSentence is not a Clause.

assert

     public void assert(ClauseSet cls) throws IllegalArgumentException

  This function can be used to add knowledge to this KnowledgeBase. It will add all the Clauses in the given ClauseSet to this ClauseSet.

  Parameters:
    cls - the ClauseSet containing the new Clauses
  Throws: IllegalArgumentException
    An exception will occur if the given ClauseSet is null.

isInconsistent

     public boolean isInconsistent() throws IOException

  This function tests whether this KnowledgeBase is inconsistent.

  Returns:
    `true` iff this KnowledgeBase is inconsistent
  Throws: IOException
    An exception can occur if writing to the given OutputStream for tracing fails.

evaluate

     public boolean evaluate(KRSentence sent) throws IllegalArgumentException, FormalismException, IOException

  This function takes a Clause and evaluates it against this ClauseSet. It returns whether the given Clause is entailed by this ClauseSet.

  Parameters:
    sent - the Clause to be evaluated
  Returns:
    `true` iff the given Clause could be derived from the ClauseSet
  Throws: IllegalArgumentException
    An exception will occur if the given Clause is null.
  Throws: FormalismException
    An exception will occur if the given KRSentence is not a Clause.
  Throws: IOException
    An exception can occur if writing to the given OutputStream for tracing fails.

sentences

     public Enumeration sentences()

  This function returns an Enumerator for the Clauses in this ClauseSet.

  Returns:
    an Enumeration for the KRSentences in this KnowledgeBase

setTraceStream

     public void setTraceStream(OutputStream ost)

  This function can be used create a trace of the functions `isInconsistent()` and `evaluate()`. If the given value is null no trace will be generated. Otherwise the trace will be written to the given OutputStream.

  Parameters:
    ost - the OutputStream the trace is to be written to

writeToStream

     public void writeToStream(OutputStream os) throws IllegalArgumentException, IOException

  This function writes the content of this KnowledgeBase to the given OutputStream.

  Parameters:
    os - theOutputStream the Clauses are to be written to
  Throws: IllegalArgumentException
    An exception will occur if the given OutputStream is null.
  Throws: IOException
    An exception will occur if writing to the given OutputStream failed for some reason.

parse

     public static ClauseSet parse(InputStream ist) throws IllegalArgumentException, IOException, ParseException

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

       <clauseset> ::= CLAUSESET <clause>*
       <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 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