    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

A FormulaSet is a set of Formulae. This is the most general knowledge representation in the fopl package. When evaluating a Formula against a FormulaSet, the Formula and FormulaSet will be converted to clause form and a resolution theorem prover will be used to test whether the negated Formula and the FormulaSet give rise to an inconsistency.

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.

##

FormulaSet

     public FormulaSet()

  This constructor creates an empty FormulaSet.

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.

##

clone

     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

assert

     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.

getFOPLFormula

     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.

isInconsistent

     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.

evaluate

     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.

evaluate

     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.

usedInProof

     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

sentences

     public Enumeration sentences()

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

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

parse

     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