All Packages  Class Hierarchy  This Package  Previous  Next  Index

Class JavaAgent.resource.fopl.FormulaSet

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

public class FormulaSet

extends Object

implements Parsable, KnowledgeBase

See Also:

Formula, ClauseSet, RTProver

FormulaSet()

This constructor creates an empty FormulaSet.

FormulaSet(Formula)

This constructor creates a FormulaSet that contains just the given Formula.

assert(KRSentence)

This function can be used to add knowledge to this FormulaSet.

clone()

Cloning a FormulaSet returns a new FormulaSet consisting of clones of the Formulae in the original FormulaSet.

evaluate(KRSentence)

This function takes a Formula and evaluates it against this FormulaSet.

evaluate(KRSentence, Vector)

This function tries to find values for the Variables in the given Vector such that the given KRSentence follows from this FormulaSet.

getFOPLFormula(KRSentence)

This function converts the given KRSentence into a FOPLFormula.

isInconsistent()

This function tests whether this FormulaSet is inconsistent.

parse(InputStream)

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

sentences()

This function returns an enumerator for the Formulae in this FormulaSet.

setTraceStream(OutputStream)

This function can be used create a trace of the functions isInconsistent() and evaluate().

usedInProof(KRSentence)

This function tests whether the given KRSentence was used in the last derivation or whether it could have been deleted from this FormulaSet without changing the derivability of the last query.

writeToStream(OutputStream)

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

 public FormulaSet()

This constructor creates an empty FormulaSet.

 public FormulaSet(Formula aFrom) throws IllegalArgumentException

This constructor creates a FormulaSet that contains just the given Formula.

Parameters:

aFrom - the Formula in this FormulaSet

Throws: IllegalArgumentException

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

 public Object clone()

Cloning a FormulaSet returns a new FormulaSet consisting of clones of the Formulae in the original FormulaSet.

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 FormulaSet.

Parameters:

sent - the KRSentence 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 Formula.

 protected static FOPLFormula getFOPLFormula(KRSentence sent) throws FormalismException

This function converts the given KRSentence into a FOPLFormula. It trivially succeeds if the given KRSentence already is a FOPLFormula. Otherwise it tries to use the function getFOPLFormula() of the given KRSentence to get the FOPLFormula. If this fails a FormalismException will be thrown.

Parameters:

sent - the KRSentence to be converted into a FOPLFormula

Returns:

a FOPLFormula representing the given KRSentence

Throws: FormalismException

An exception will be thrown if the given KRSentence cannot be converted in to a FOPLFormula for some reason.

 public boolean isInconsistent() throws IOException

This function tests whether this FormulaSet 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 Formula and evaluates it against this FormulaSet.

Parameters:

sent - the KRSentence to be evaluated

Returns:

true iff the given KRSentence could be derived from the KnowledgeBase

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 Formula.

Throws: IOException

An exception can occur if writing to the given OutputStream for tracing fails.

 public Hashtable evaluate(KRSentence sent,
                           Vector vars) throws IllegalArgumentException, FormalismException, IOException

This function tries to find values for the Variables in the given Vector such that the given KRSentence follows from this FormulaSet. The values will be returned in a HashTable. If no such values can be found the result will be null.

Parameters:

sent - the KRSentence to be evaluated

vars - The Vector of Variables

Returns:

a HashTable containing the Variable value assignments found or null if no assignments were found.

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 Formula.

Throws: IOException

An exception can occur if writing to the given OutputStream for tracing fails.

 public boolean usedInProof(KRSentence krs)

This function tests whether the given KRSentence was used in the last derivation or whether it could have been deleted from this FormulaSet without changing the derivability of the last query.

Parameters:

krs - the KRSentence to be tested

Returns:

true iff it was used in the derivation

 public Enumeration sentences()

This function returns an enumerator for the Formulae in this FormulaSet.

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 KRSentences is 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 FormulaSet parse(InputStream ist) throws IllegalArgumentException, IOException, ParseException

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

 <formulaset>::= FORMS <formula>*
 <formula>    ::= ( <quant> <c-from> ) | <c-from>
 <quant>      ::= ( <quantifier> <varspec>+ )
 <quantifier> ::= forall | exists
 <varspec>    ::= <variable> | 
                  ( <variable> <constant> )
 <c-from>     ::= <literal> |
                  ( not <formula> ) | 
                  ( and <formula> <formula>+ ) | 
                  ( or <formula> <formula>+ ) | 
                  ( implies <formula> <formula> ) | 
                  ( iff <formula> <formula> ) | 
                  ( xor <formula> <formula> ) | 
 <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