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

Variable Index

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

Constructor Index

o RTProver()
This constructor creates an RTProver.

Method Index

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

Variables

o searchLimit 
 protected static int searchLimit
the maximum number of Clauses that will be explored

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

o open 
 protected Vector open
the Vector of open Clauses

o closed 
 protected Vector closed
the Vector of closed Clauses

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

Constructors

o RTProver 
 public RTProver()
This constructor creates an RTProver.

Methods

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