Goéland

Goéland is an automated theorem prover using the tableau method for first order logic.

It supports TPTP FOF files (TFF/THF files will be supported in a future version).

License

Goéland is licensed under the CeCILL 2.1 License. See LICENSE.

Installation

Dependencies

Goéland needs Go (version >= 1.13, download directly from the site) and goyacc (sudo apt-get install golang-golang-x-tools) to compile.

Compilation

Proceed as follows to build Goéland from source (assuming that you currently are in the root folder of the repository):

$ cd src
$ make

This should produce an executable in the _build folder, and .so libraries for each module in the plugins folder.

You can now run Goéland:

$ ./_build/goeland -h
Usage of ./_build/goeland:
[...]

Usage

This is still a preliminary version of the implementation. Goéland must be called from the command line. To solve a problem.p problem, just give this problem as an argument:

$ ./_build/goeland problem.p

By default, this will run Goéland, with all its extensions, on the problem. Beware that currently, includes statements in TPTP problem files aren't managed by the parser. It is scheduled to be added in the near future. For the moment, the python script add_include.py can do this job if needed.

Parameters

The parameters must be passed before the problem file. The available parameters are as follows:

Result values

Since the tableau method only proves theorems, Goéland returns Valid when a proof is found, otherwise it loops to infinity, trying to increase the reintroduction limit.