Tweety
A comprehensive collection of Java libraries for logical aspects of artificial intelligence and knowledge representation
Home Libraries Downloads Documentation Web Interfaces Contact


Brought to you by




Supported by

back

Integration of FOL Theorem Provers

Tweety supports the integration of different first-order Theorem provers in order to perform reasoning tasks in first-order logic. It is required that at least one FOL theorem prover is explicitly configured as default prover.

Tweety has built-in support for a naive prover that computes models of formulas via a brute-force search. This prover is also initially configured as default prover. However, whenever you perform a reasoning task that involves a FOL theorem prover, a warning message is printed out that no FOL theorem prover is configured and the naive prover is used as a default. If you do not care about performance issues and only want to get rid of the warning message, you should configure the naive prover as your default FOL theorem prover explicitly. To do that, simply add the following lines somewhere before you invoke your reasoning task for the first time:

import net.sf.tweety.logics.fol.prover.*;
...
FolTheoremProver.setDefaultProver(new NaiveProver());

However, depending on your reasoning tasks it is recommend that you set another FOL theorem prover as your default prover. Tweety also supports the integration of command-line based provers such as EProver and Prover9. If you have one of those installed in your system you can set it as your default FOL theorem prover solver via:

FolTheoremProver.setDefaultProver(new EProver(pathToEProver));

or

FolTheoremProver.setDefaultProver(new Prover9(pathToProver9));

If your favorite FOL theorem prover is not supported, please have a look at the FolTheoremProver.java interface in the net.sf.tweety.logics.fol.prover package and think about implementing a bridge yourself and contribute it to Tweety.




back



Last updated 06.07.2016, Matthias Thimm