    All Packages  Class Hierarchy  This Package  Previous  Next  Index

# Class JavaAgent.resource.fopl.RTProver

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

public class RTProver
extends Object

An RTProver is a resolution theorem prover. Currently it maintains two Vectors of Clauses, the open and closed Clauses. Clauses can be added to either Vector with the appropriate add-functions. Once the RTProver is set up in this way the function `resolve()` can be called to start the reasoning process.

The basic strategy is very simple. The RTProver takes the first Clause from the Vector of open Clauses and generates all resolvents with Clauses from the Vector of closed Clauses over only one of the Literals in the former Clause (the one that generates the fewest successors). The first Clause in the Vector of open Clauses is then moved to the Vector of closed Clausesand the new Clauses are added to the Vector of open Clauses. This process is repeated with the first Clause in the Vector of open Clauses until either the empty Clause has been generated, or until the Vector of open Clauses is empty.

See Also:
  Clause

##

closed
  the Vector of closed Clauses
containsEmptyClause
  this boolean indicates whether the open or closed Clauses contain the empty Clause
lastRefute
  a Vector of Clauses that represent the last refutation by this RTProver
open
  the Vector of open Clauses
searchLimit
  the maximum number of Clauses that will be explored

##

RTProver()
  This constructor creates an RTProver.

##

addClosedClause(Clause)
  This function can be used to add Clauses to the Vector of closed Clauses.
addOpenClause(Clause)
  This function can be used to add Clauses to the Vector of open Clauses.
extractRefutation()
  This function extracts a proof from the Clauses currently in the closed and open sets.
extractValues(Vector)
  This function extracts the values for the given Variables from the last refutation.
resolve()
  This function executes the resolution theorem proving process.
setSearchLimit(int)
  This function can be used to set the search limit for this RTProver.
setTraceStream(OutputStream)
  This function can be used create a trace of the function `resolve()`.
usedInProof(KRSentence)
  This function tests whether the given KRSentence was used in the last derivation.

##

searchLimit

     protected static int searchLimit

  the maximum number of Clauses that will be explored

lastRefute

     protected Vector lastRefute

  a Vector of Clauses that represent the last refutation by this RTProver

open

     protected Vector open

  the Vector of open Clauses

closed

     protected Vector closed

  the Vector of closed Clauses

containsEmptyClause

     protected boolean containsEmptyClause

  this boolean indicates whether the open or closed Clauses contain the empty Clause

##

RTProver

     public RTProver()

  This constructor creates an RTProver.

##

addOpenClause

     public void addOpenClause(Clause aClause) throws IllegalArgumentException

  This function can be used to add Clauses to the Vector of open Clauses.

  Parameters:
    aClause - the Clause to be added
  Throws: IllegalArgumentException
    An exception will occur if the given Clause is null.

addClosedClause

     public void addClosedClause(Clause aClause) throws IllegalArgumentException

  This function can be used to add Clauses to the Vector of closed Clauses.

  Parameters:
    aClause - the Clause to be added
  Throws: IllegalArgumentException
    An exception will occur if the given Clause is null.

resolve

     public boolean resolve() throws IOException

  This function executes the resolution theorem proving process. The basic strategy is outlined above. The process stops when there are no more open Clauses and returns `true` indicating satisfyability. If it stops because the empty Clause has been generated it will return `false` indicating inconsistency.

  Returns:
    `false` if the given Clauses were inconsistent
  Throws: IOException
    An exception can occur if writing to the given OutputStream for tracing fails.

extractRefutation

     protected Vector extractRefutation()

  This function extracts a proof from the Clauses currently in the closed and open sets. The last open Clause should be the empty Clause. The result is a Vector that contains all those Clauses that were involved in the proof (in the order they were generated).

  Returns:
    A vector with all Clauses involved in the proof

extractValues

     public Hashtable extractValues(Vector vars)

  This function extracts the values for the given Variables from the last refutation. It returns a Hashtable in which Variables are mapped to Terms. It cannot be guaranteed that given Variables will occor in the Hashtable or that they will be mapped to a value.

  Parameters:
    vars - a Vector of Variables
  Returns:
    a Hashtable containing the Terms the given Variables were mapped to.

usedInProof

     public boolean usedInProof(KRSentence krs)

  This function tests whether the given KRSentence was used in the last derivation.

  Parameters:
    krs - the KRSentence to be tested
  Returns:
    true iff it was used in the derivation

setSearchLimit

     public void setSearchLimit(int limit)

  This function can be used to set the search limit for this RTProver. Effectively, this limits the number of Clauses that can be in the set of closed nodes. Note that this set is not empty to start with.

  Parameters:
    limit - the search limit

setTraceStream

     public void setTraceStream(OutputStream ost)

  This function can be used create a trace of the function `resolve()`. 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

    All Packages  Class Hierarchy  This Package  Previous  Next  Index