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:
...
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:
or
If your favorite FOL theorem prover is not supported, please have a look at the FolReasoner.java interface in the org.tweetyproject.logics.fol.prover package and think about implementing a bridge yourself and contribute it to TweetyProject.
back