ai.krr.propositions
Class RTPSolverIE

java.lang.Object
  ai.krr.propositions.RTPSolverIE

All Implemented Interfaces:

TheoremProver

public class RTPSolverIE
extends java.lang.Object
implements TheoremProver

Nested Class Summary

protected class

RTPSolverIE.DerivedClause

Field Summary

(package private) static java.lang.String[]	examples
protected java.io.OutputStream	traceStream the stream to which trace output should be written or null, the default value, for no tracing

Constructor Summary

RTPSolverIE()
This constructor creates a new TheoremProver that uses the resolution rule to find a refutation for a set of propositional Clauses.

Method Summary

protected java.lang.Object	clone() This class does not support cloning and an exception will be thrown if this method is called.
boolean	equivalent(Sentence stmt1, Sentence stmt2) This function tests whether the two given Sentences are equivalent.
boolean	follows(Sentence stmt, java.util.Collection<Sentence> axioms) This function tests whether the given Sentence logically follows from the given Collection of Sentences.
Interpretation	getModel(java.util.List<Clause> clauses) This function attempts to find a model for the given Set of Clauses.
java.util.Map<java.lang.Integer,BooleanSymbol>	getModel(java.util.List<IntEncodedClause> clauses, int maxPropInt) This function attempts to find a model for the given Set of Clauses.
Interpretation	getModel(Sentence stmt) This function attempts to find a model for the given Sentence.
protected static IntEncodedClause	getNonTautologyResolvent(IntEncodedClause clause1, IntEncodedClause clause2)
java.util.List<IntEncodedClause>	getRefutation(java.util.List<Clause> clauses)
java.util.Set<IntEncodedClause>	getRefutation(java.util.List<IntEncodedClause> clauses, int maxPropInt)
boolean	isInconsistent(Sentence stmt) This function tests whether the given Sentence in propositional logic is inconsistent.
boolean	isValid(Sentence stmt) This function tests whether the given Sentence in propositional logic is valid.
static void	main(java.lang.String[] args)
protected void	printTrace(java.lang.String msg) This function must be called to print out tracing messages.
void	setTraceStream(java.io.OutputStream stream) This function can be used to activate tracing of the search activity.
void	terminate() This function can be used to terminate the search for a model.

Methods inherited from class java.lang.Object

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

Field Detail

traceStream

protected java.io.OutputStream traceStream

the stream to which trace output should be written or null, the default value, for no tracing

examples

static final java.lang.String[] examples

Constructor Detail

RTPSolverIE

public RTPSolverIE()

This constructor creates a new TheoremProver that uses the resolution rule to find a refutation for a set of propositional Clauses.

Method Detail

clone

protected java.lang.Object clone()
                          throws java.lang.CloneNotSupportedException

This class does not support cloning and an exception will be thrown if this method is called.

Overrides:

clone in class java.lang.Object

Returns:

nothing

Throws:

java.lang.CloneNotSupportedException - will be thrown

isValid

public boolean isValid(Sentence stmt)

This function tests whether the given Sentence in propositional logic is valid. A Sentence is valid if and only if it is true under all possible Interpretations.

Specified by:

isValid in interface TheoremProver

Parameters:

stmt - the Sentence to be tested

Returns:

whether the given sentence is a tautology

isInconsistent

public boolean isInconsistent(Sentence stmt)

This function tests whether the given Sentence in propositional logic is inconsistent. A Sentence is inconsistent if and only if it is false under all possible Interpretations.

Specified by:

isInconsistent in interface TheoremProver

Parameters:

stmt - the Sentence to be tested

Returns:

whether the given sentence is a contradiction

getModel

public Interpretation getModel(Sentence stmt)

This function attempts to find a model for the given Sentence. A model is an Interpretation under which the Sentence evaluates to true. If such a model exists, the Sentence is satisfiable and the returned Interpretation proves this. If the Sentence is inconsistent then there is no model and this function returns null.

Specified by:

getModel in interface TheoremProver

Parameters:

stmt - the Sentence for which a model is sought

Returns:

an Interpretation that satisfies the given Sentence, or null iff the Sentence is inconsistent

equivalent

public boolean equivalent(Sentence stmt1,
                          Sentence stmt2)

This function tests whether the two given Sentences are equivalent. Two Sentences are equivalent if they evaluate to the same truth value under all possible Interpretations.

Specified by:

equivalent in interface TheoremProver

Parameters:

stmt1 - the Sentence that may be equivalent to stmt2

stmt2 - the Sentence that may be equivalent to stmt1

Returns:

whether stmt1 and stmt2 are equivalent

follows

public boolean follows(Sentence stmt,
                       java.util.Collection<Sentence> axioms)

This function tests whether the given Sentence logically follows from the given Collection of Sentences.

Specified by:

follows in interface TheoremProver

Parameters:

stmt - the Sentence to be tested

axioms - Sentences from which the axiom might follow

Returns:

whether stmt logically follows from axioms

setTraceStream

public void setTraceStream(java.io.OutputStream stream)

This function can be used to activate tracing of the search activity. Setting the trace stream to null switches off tracing completely. Otherwise a trace is written to the given stream.

Parameters:

stream - the OutputStream to which the trace should be written or null for no tracing

getRefutation

public java.util.List<IntEncodedClause> getRefutation(java.util.List<Clause> clauses)

getModel

public Interpretation getModel(java.util.List<Clause> clauses)

This function attempts to find a model for the given Set of Clauses. A model is an Interpretation under which all the Clauses evaluate to true. If such a model exists, the Set of Clauses is satisfiable and the returned Interpretation proves this. If the Set of Clauses is inconsistent then there is no model and this function returns null.

Parameters:

clauses - the Set of Clauses for which a model is sought

Returns:

an Interpretation that satisfies the given Set of Clauses, or null iff the Set of Clauses is inconsistent

getModel

public java.util.Map<java.lang.Integer,BooleanSymbol> getModel(java.util.List<IntEncodedClause> clauses,
                                                               int maxPropInt)

This function attempts to find a model for the given Set of Clauses. A model is an Interpretation under which all the Clauses evaluate to true. If such a model exists, the Set of Clauses is satisfiable and the returned Interpretation proves this. If the Set of Clauses is inconsistent then there is no model and this function returns null.

Parameters:

clauses - the Set of Clauses for which a model is sought

Returns:

an Interpretation that satisfies the given Set of Clauses, or null iff the Set of Clauses is inconsistent

getRefutation

public java.util.Set<IntEncodedClause> getRefutation(java.util.List<IntEncodedClause> clauses,
                                                     int maxPropInt)

terminate

public void terminate()

This function can be used to terminate the search for a model. This may not terminate the search immediately but only sets an appropriate flag for the SerchEngine used internally. When the search for a model returns after being terminated (from a different Thread) the returned result will be null.

printTrace

protected void printTrace(java.lang.String msg)

This function must be called to print out tracing messages. Note that this function does not test whether tracing has been switched off, i.e. whether traceStream==null.

Parameters:

msg - the message to be printed to the trace stream

getNonTautologyResolvent

protected static IntEncodedClause getNonTautologyResolvent(IntEncodedClause clause1,
                                                           IntEncodedClause clause2)

main

public static void main(java.lang.String[] args)