public class EProver
extends java.lang.Object
Constructor and Description |
---|
EProver(java.lang.String executable)
Create a running instance of EProver based on existing batch
specification file.
|
EProver(java.lang.String executable,
java.lang.String kbFile)
Create a new batch specification file, and create a new running
instance of EProver.
|
Modifier and Type | Method and Description |
---|---|
static void |
addBatchConfig(java.lang.String inputFilename,
int timeout)
Update batch specification file.
|
java.lang.String |
assertFormula(java.lang.String formula)
Add an assertion for inference.
|
boolean |
assertFormula(java.lang.String userAssertionTPTP,
KB kb,
EProver eprover,
java.util.ArrayList<Formula> parsedFormulas,
boolean tptp)
Add an assertion for inference.
|
static void |
main(java.lang.String[] args)
A simple test.
|
java.lang.String |
submitQuery(java.lang.String formula,
KB kb)
Submit a query.
|
void |
terminate()
Terminate this instance of EProver.
|
static void |
writeBatchConfig(java.lang.String inputFilename,
int timeout)
Create a new batch specification file.
|
public EProver(java.lang.String executable, java.lang.String kbFile) throws java.io.IOException
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.java.io.IOException
- should not normally be thrown unless either
EProver executable or database file name are incorrect
e_ltb_runner -- interactive LTBSampleInput-AP.txtpublic EProver(java.lang.String executable) throws java.io.IOException
executable
- A File object denoting the platform-specific
EProver executable.java.io.IOException
public static void writeBatchConfig(java.lang.String inputFilename, int timeout)
inputFilename
- contains TPTP assertionstimeout
- time limit in Epublic static void addBatchConfig(java.lang.String inputFilename, int timeout)
inputFilename
- contains TPTP assertionstimeout
- time limit in Epublic java.lang.String assertFormula(java.lang.String formula)
formula
- asserted formula in the KIF syntaxjava.io.IOException
- should not normally be thrownpublic boolean assertFormula(java.lang.String userAssertionTPTP, KB kb, EProver eprover, java.util.ArrayList<Formula> parsedFormulas, boolean tptp)
userAssertionTPTP
- asserted formula in the TPTP syntaxkb
- Knowledge baseeprover
- an instance of EProverparsedFormulas
- a lit of parsed formulas in KIF syntaxtptp
- convert formula to TPTP if tptp = truepublic void terminate() throws java.io.IOException
java.io.IOException
- should not normally be thrownpublic java.lang.String submitQuery(java.lang.String formula, KB kb)
formula
- query in the KIF syntaxkb
- current knowledge basejava.io.IOException
- should not normally be thrownpublic static void main(java.lang.String[] args) throws java.lang.Exception
java.lang.Exception