ai.krr.fol
Class HerbrandGenerator

java.lang.Object
  ai.krr.fol.HerbrandGenerator

All Implemented Interfaces:

TheoremProver

public class HerbrandGenerator
extends java.lang.Object
implements TheoremProver

Nested Class Summary

(package private) static class

HerbrandGenerator.HerbrandUniverse

Field Summary

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

Constructor Summary

HerbrandGenerator()

Method Summary

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.
protected static java.util.List<Clause>	getGroundInstances(java.util.Set<Clause> clauses, HerbrandGenerator.HerbrandUniverse hu)
boolean	isInconsistent(Sentence stmt) This function tests whether the given Sentence in first-order logic is inconsistent.
boolean	isInconsistent(java.util.Set<Clause> clauses)
boolean	isValid(Sentence stmt) This function tests whether the given Sentence in first-order logic is valid.
void	printTrace(java.lang.String msg) This function must be called to print out tracing messages.
void	setHuLimit(int limit)
void	setTraceStream(java.io.OutputStream stream) This function can be used to activate tracing of the search activity.

Methods inherited from class java.lang.Object

clone, 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

HUL

protected int HUL

Constructor Detail

HerbrandGenerator

public HerbrandGenerator()

Method Detail

isValid

public boolean isValid(Sentence stmt)

Description copied from interface: TheoremProver

This function tests whether the given Sentence in first-order 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

equivalent

public boolean equivalent(Sentence stmt1,
                          Sentence stmt2)

Description copied from interface: TheoremProver

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)

Description copied from interface: TheoremProver

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

isInconsistent

public boolean isInconsistent(Sentence stmt)

Description copied from interface: TheoremProver

This function tests whether the given Sentence in first-order 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

isInconsistent

public boolean isInconsistent(java.util.Set<Clause> clauses)

setHuLimit

public void setHuLimit(int limit)

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

printTrace

public 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

getGroundInstances

protected static java.util.List<Clause> getGroundInstances(java.util.Set<Clause> clauses,
                                                           HerbrandGenerator.HerbrandUniverse hu)