com.articulate.sigma

Class EProver

java.lang.Object

com.articulate.sigma.EProver

public class EProver
extends Object

Constructor Summary

Constructors

Constructor and Description
EProver(String executable) Create a running instance of EProver based on existing batch specification file.
EProver(String executable, String kbFile) Create a new batch specification file, and create a new running instance of EProver.

Method Summary

Modifier and Type	Method and Description
static void	addBatchConfig(String inputFilename, int timeout) Update batch specification file.
String	assertFormula(String formula) Add an assertion for inference.
boolean	assertFormula(String userAssertionTPTP, KB kb, EProver eprover, ArrayList<Formula> parsedFormulas, boolean tptp) Add an assertion for inference.
static void	main(String[] args) A simple test.
String	submitQuery(String formula, KB kb) Submit a query.
void	terminate() Terminate this instance of EProver.
static void	writeBatchConfig(String inputFilename, int timeout) Create a new batch specification file.

Methods inherited from class java.lang.Object

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

Constructor Detail

EProver

public EProver(String executable,
               String kbFile)
        throws IOException

Create a new batch specification file, and create a new running instance of EProver.

Parameters:

executable - A File object denoting the platform-specific EProver executable.

kbFile - A File object denoting the initial knowledge base to be loaded by the EProver executable.

Throws:

IOException - should not normally be thrown unless either EProver executable or database file name are incorrect e_ltb_runner -- interactive LTBSampleInput-AP.txt

EProver

public EProver(String executable)
        throws IOException

Create a running instance of EProver based on existing batch specification file.

Parameters:

executable - A File object denoting the platform-specific EProver executable.

Throws:

IOException

Method Detail

writeBatchConfig

public static void writeBatchConfig(String inputFilename,
                                    int timeout)

Create a new batch specification file. e_ltb_runner processes a batch specification file; it contains a specification of the background theory, some options, and a number of individual job requests. It is used with the option --interactive.

Parameters:

inputFilename - contains TPTP assertions

timeout - time limit in E

addBatchConfig

public static void addBatchConfig(String inputFilename,
                                  int timeout)

Update batch specification file. "inputFilename" is added into existing batch specification file for inference.

Parameters:

inputFilename - contains TPTP assertions

timeout - time limit in E

assertFormula

public String assertFormula(String formula)

Add an assertion for inference.

Parameters:

formula - asserted formula in the KIF syntax

Returns:

answer to the assertion (in the XML syntax)

Throws:

IOException - should not normally be thrown

assertFormula

public boolean assertFormula(String userAssertionTPTP,
                             KB kb,
                             EProver eprover,
                             ArrayList<Formula> parsedFormulas,
                             boolean tptp)

Add an assertion for inference.

Parameters:

userAssertionTPTP - asserted formula in the TPTP syntax

kb - Knowledge base

eprover - an instance of EProver

parsedFormulas - a lit of parsed formulas in KIF syntax

tptp - convert formula to TPTP if tptp = true

Returns:

true if all assertions are added for inference TODO: This function might not be necessary if we find a way to directly add assertion into opened inference engine (e_ltb_runner)

terminate

public void terminate()
               throws IOException

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

Throws:

IOException - should not normally be thrown

submitQuery

public String submitQuery(String formula,
                          KB kb)

Submit a query.

Parameters:

formula - query in the KIF syntax

kb - current knowledge base

Returns:

answer to the query

Throws:

IOException - should not normally be thrown

main

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

A simple test. Works as follows:

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

Throws:

Exception