ai.krr.propositions
Class DPSolverIE

java.lang.Object
  extended by ai.krr.propositions.DPSolverIE
All Implemented Interfaces:
TheoremProver

public class DPSolverIE
extends java.lang.Object
implements TheoremProver


Field Summary
protected  ai.search.SearchEngineForIntCostFn<ai.krr.propositions.DPSolverIE.DPState> searcher
          the SearchEngine used to perform the search for a model
protected  java.io.OutputStream traceStream
          the stream to which trace output should be written or null, the default value, for no tracing
 
Constructor Summary
DPSolverIE()
           This constructor creates a new TheoremProver that uses the method of Davis and Putnam to find a model 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.
 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.
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

searcher

protected ai.search.SearchEngineForIntCostFn<ai.krr.propositions.DPSolverIE.DPState> searcher
the SearchEngine used to perform the search for a model


traceStream

protected java.io.OutputStream traceStream
the stream to which trace output should be written or null, the default value, for no tracing

Constructor Detail

DPSolverIE

public DPSolverIE()

This constructor creates a new TheoremProver that uses the method of Davis and Putnam to find a model 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

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

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