net.sf.tweety.logics.fol.prover

Class EProver

java.lang.Object

net.sf.tweety.logics.fol.prover.FolTheoremProver

net.sf.tweety.logics.fol.prover.EProver

public class EProver
extends FolTheoremProver

Invokes Eprover (http://eprover.org) and returns its results.

Author:

Bastian Wolf, Nils Geilen, Matthias Thimm

Field Summary

Fields

Modifier and Type	Field and Description
private java.lang.String	additionalArguments Additional arguments for the call to the eprover binary (Default value is "--auto-schedule" which seems to be working best in general)
private Shell	bash Shell to run eprover
private java.lang.String	binaryLocation String representation of the E binary path, directory, where the temporary files are stored

Fields inherited from class net.sf.tweety.logics.fol.prover.FolTheoremProver

defaultProver

Constructor Summary

Constructors

Constructor and Description
EProver(java.lang.String binaryLocation) Constructs a new instance pointing to a specific eprover
EProver(java.lang.String binaryLocation, Shell bash) Constructs a new instance pointing to a specific eprover

Method Summary

Modifier and Type	Method and Description
boolean	equivalent(FolBeliefSet kb, FolFormula a, FolFormula b)
java.lang.String	getAdditionalArguments() Returns the additional arguments given to the call of the eprover binary (Default value is "--auto-schedule")
java.lang.String	getBinaryLocation() returns the path of the provers binary
boolean	query(FolBeliefSet kb, FolFormula query) This method determines the answer of the given query wrt.
void	setAdditionalArguments(java.lang.String s) Sets the additional arguments given to the call of the eprover binary (Default value is "--auto-schedule")
void	setBinaryLocation(java.lang.String binaryLocation) Change path of the binary

Methods inherited from class net.sf.tweety.logics.fol.prover.FolTheoremProver

getDefaultProver, setDefaultProver

Methods inherited from class java.lang.Object

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

Field Detail

binaryLocation

private java.lang.String binaryLocation

String representation of the E binary path, directory, where the temporary files are stored

additionalArguments

private java.lang.String additionalArguments

Additional arguments for the call to the eprover binary (Default value is "--auto-schedule" which seems to be working best in general)

bash

private Shell bash

Shell to run eprover

Constructor Detail

EProver

public EProver(java.lang.String binaryLocation,
               Shell bash)

Constructs a new instance pointing to a specific eprover

Parameters:

binaryLocation - of the eprover executable on the hard drive

bash - shell to run commands

EProver

public EProver(java.lang.String binaryLocation)

Constructs a new instance pointing to a specific eprover

Parameters:

binaryLocation - of the eprover executable on the hard drive

Method Detail

setAdditionalArguments

public void setAdditionalArguments(java.lang.String s)

Sets the additional arguments given to the call of the eprover binary (Default value is "--auto-schedule")

Parameters:

s - some string

getAdditionalArguments

public java.lang.String getAdditionalArguments()

Returns the additional arguments given to the call of the eprover binary (Default value is "--auto-schedule")

query

public boolean query(FolBeliefSet kb,
                     FolFormula query)

Description copied from class: FolTheoremProver

This method determines the answer of the given query wrt. to the given knowledge base.

Specified by:

query in class FolTheoremProver

Parameters:

kb - the knowledge base

query - a query.

Returns:

the answer to the query.

equivalent

public boolean equivalent(FolBeliefSet kb,
                          FolFormula a,
                          FolFormula b)

Specified by:

equivalent in class FolTheoremProver

getBinaryLocation

public java.lang.String getBinaryLocation()

returns the path of the provers binary

Returns:

the path of the provers binary

setBinaryLocation

public void setBinaryLocation(java.lang.String binaryLocation)

Change path of the binary

Parameters:

binaryLocation - the new path of the E binary