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

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.

 public ClauseSet()

This constructor creates an empty 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.

 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.

 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.

 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

 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.

 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.

 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.

 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.

 public Enumeration sentences()

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

Returns:

an Enumeration for the KRSentences in this KnowledgeBase

 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

 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.

 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