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

Brought to you by

Supported by


Integration of FOL Theorem Provers

TweetyProject 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.

TweetyProject 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 org.tweetyproject.logics.fol.reasoner.*;
FolReasoner.setDefaultProver(new SimpleFolReasoner());

However, depending on your reasoning tasks it is recommend that you set another FOL theorem prover as your default prover. TweetyProject 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:

FolReasoner.setDefaultProver(new EProver(pathToEProver));


FolReasoner.setDefaultProver(new Prover9(pathToProver9));

If your favorite FOL theorem prover is not supported, please have a look at the interface in the org.tweetyproject.logics.fol.prover package and think about implementing a bridge yourself and contribute it to TweetyProject.


Last updated 28.01.2021, Anna Gessler | Terms