jtp.gmp
Class Utils

java.lang.Object
  |
  +--jtp.gmp.Utils

public class Utils

extends Object

Utils.java Created: Thu Jan 4 02:24:58 2001

Constructor Summary

Utils()

Method Summary

static ReasoningStep	deriveFrom(Literal goal, ReasoningStep subStep)
static ReasoningStep	deriveFrom(Literal goal, ReasoningStep subStep, List varStack) tries to derive a proof for a literal from a pre-existing reasoning step.
static ReasoningStep	deriveFrom(Literal goal, ReasoningStep subStep, List varStack, ModusPonensProofStep reusableStep) tries to derive a proof for a literal from a pre-existing reasoning step.
static void	restoreVariableSet(Collection vars) Restores the variables modified by unify(jtp.fol.Literal, jtp.gmp.ClauseOrientation, java.util.Collection, java.util.List) to pristine condition.
static boolean	unify(Literal goal, ClauseOrientation hc, Collection vars, List varStack) Performs unification of a goal with the head of the clause orientation.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

Utils

public Utils()

Method Detail

unify

public static boolean unify(Literal goal,
                            ClauseOrientation hc,
                            Collection vars,
                            List varStack)

Performs unification of a goal with the head of the clause orientation. First of all, we collect all the variables in the clause into the supplied collection. These variables will be replaced by new ones before unification. This is done by assigning them values (new variables), and then dereferencing the clause. Note that the clause is now modified (its variables are bound). To restore it to pristine condition, call restoreVariableSet(java.util.Collection) on the collection (whether or not the operation succeeded). The resulting variable bindings can be used in modus ponens reasoning or other forms of resolution. Note that this function ignores the literal's relation symbol and polarity - this is supposed to have been taken care of by the KB indexing mechanism!

Parameters:

goal - the goal to unify with the clause.

hc - the clause orientation

vars - the collection of the variables found in the clause.

varStack - will hold the list of bound variables from both the literal and the clause, if the operation succeeds.

Returns:

success status.

deriveFrom

public static ReasoningStep deriveFrom(Literal goal,
                                       ReasoningStep subStep)

deriveFrom

public static ReasoningStep deriveFrom(Literal goal,
                                       ReasoningStep subStep,
                                       List varStack)

tries to derive a proof for a literal from a pre-existing reasoning step. The goal literal is unified with the claim of the reasoning step; if the unification is succesful, a new modus ponens reasoning step is created, with the old reasoning step as a sub-proof.

Parameters:

goal - the literal that we are trying to derive.

subStep - the pre-existing reasoning step

varStack - the variable stack to use.

deriveFrom

public static ReasoningStep deriveFrom(Literal goal,
                                       ReasoningStep subStep,
                                       List varStack,
                                       ModusPonensProofStep reusableStep)

tries to derive a proof for a literal from a pre-existing reasoning step. The goal literal is unified with the claim of the reasoning step; if the unification is succesful, a new modus ponens reasoning step is created, with the old reasoning step as a sub-proof. This form of method tries to reuse an existing ModusPonensProofStep. The supplied reasoning step is reused if:

1. it is not null,
2. Unification has been performed (if not, the subStep is returned instead.)

   Parameters:

   goal - the literal that we are trying to derive.

   subStep - the pre-existing reasoning step

   varStack - the variable stack to use.

   reusableStep - try and reuse this reasoning step, if not null.

restoreVariableSet

public static void restoreVariableSet(Collection vars)

Restores the variables modified by unify(jtp.fol.Literal, jtp.gmp.ClauseOrientation, java.util.Collection, java.util.List) to pristine condition. Variables are all unbound, and the collection is cleared.

Parameters:

vars - the collection of variables to restore.