com.articulate.sigma

Class Vampire

java.lang.Object

com.articulate.sigma.InferenceEngine

com.articulate.sigma.Vampire

public class Vampire
extends InferenceEngine

Class for invoking the KIF version of Vampire from Java. Vampire takes XML input and returns XML output. Input forms are either KIF formula or KIF formula. Results of queries have the following form: KIF formula KIF formula

Note that if the result of a query is not a variable binding, then the element will be omitted.

Since:

14/08/2003, Acapulco

Author:

Andrei Voronkov

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
static class	Vampire.VampireFactory

Nested classes/interfaces inherited from class com.articulate.sigma.InferenceEngine

InferenceEngine.EngineFactory

Method Summary

Modifier and Type	Method and Description
java.lang.String	assertFormula(java.lang.String formula) Add an assertion.
static InferenceEngine.EngineFactory	getFactory()
static Vampire	getNewInstance(java.lang.String kbFileName) This static factory method returns a new Vampire instance.
static Vampire	getNewInstanceWithFormulas(java.lang.Iterable formulaSource)
static void	main(java.lang.String[] args) A simple test.
java.lang.String	submitQuery(java.lang.String formula, int timeLimit, int bindingsLimit) Submit a query.
void	terminate() Terminate this instance of Vampire.

Methods inherited from class java.lang.Object

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

Method Detail

getFactory

public static InferenceEngine.EngineFactory getFactory()

getNewInstance

public static Vampire getNewInstance(java.lang.String kbFileName)

This static factory method returns a new Vampire instance.

Parameters:

kbFileName - The complete (absolute) pathname of the KB file that will be used to populate the inference engine instance with assertions.

Throws:

java.io.IOException - should not normally be thrown unless either Vampire executable or database file name are incorrect

getNewInstanceWithFormulas

public static Vampire getNewInstanceWithFormulas(java.lang.Iterable formulaSource)

assertFormula

public java.lang.String assertFormula(java.lang.String formula)
                               throws java.io.IOException

Add an assertion.

Specified by:

assertFormula in class InferenceEngine

Parameters:

formula - asserted formula in the KIF syntax

Returns:

answer to the assertion (in the XML syntax)

Throws:

java.io.IOException - should not normally be thrown

terminate

public void terminate()
               throws java.io.IOException

Terminate this instance of Vampire. Warning:After calling this function no further assertions or queries can be done.

Overrides:

terminate in class InferenceEngine

Throws:

java.io.IOException - should not normally be thrown

submitQuery

public java.lang.String submitQuery(java.lang.String formula,
                                    int timeLimit,
                                    int bindingsLimit)
                             throws java.io.IOException

Submit a query.

Specified by:

submitQuery in class InferenceEngine

Parameters:

formula - query in the KIF syntax

timeLimit - time limit for answering the query (in seconds)

bindingsLimit - limit on the number of bindings

Returns:

answer to the query (in the XML syntax)

Throws:

java.io.IOException - should not normally be thrown

main

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

A simple test. Works as follows:

1. start Vampire;
2. make an assertion;
3. submit a query;
4. terminate Vampire.

Throws:

java.lang.Exception