Goéland v1.1

Post-release note

This release has many problematic bugs, notably ones that make Goéland inconsistent if you use the flags -inner or -preinner (see #19), or inconvenient ones such as failure in deskolemizing some problems (#16), includes with the TPTP environment variable or in the folder of the problem not working (#41), unsupported TFF1 proof search (#38) and probably many more.

We recommend either using version 1.0.0 (https://github.com/GoelandProver/Goeland/releases/tag/v1.0.0-beta.1) or the latest development version available on master (or in a PR if you need) over this version.

The current maintainer's team has taken steps to ensure that the basic functionality set always works, and to systematically test Goéland so that discovered bugs cannot happen again once they are fixed. We are very sorry for the inconvenience.

Goéand has now the following changes:

• improved options
• improved logging
• more proof output options: TPTP and LambdaPi
• Arithmetic compatibility
• more equality options
• corrected many bugs
• improved code base
• and many others

What's Changed

• Plugin Assisted by @Lluisaac in #2
• Certified Proofs by Deskolemising and its Coq Output by @jrosain in #3
• Certified proofs with Lambdapi ouput by @Lluisaac in #4
• Very Eager Closure by @Lluisaac in #5
• Dev/tstp by @jcailler in #7
• Dev/sateq improvements by @Lluisaac in #8
• Dev/incremental by @Lluisaac in #9

New Contributors

• @Lluisaac made their first contribution in #2
• @jrosain made their first contribution in #3
• @jcailler made their first contribution in #7

Full Changelog: v1.0.0-beta...v1.1

Goéland v1.0.0-beta.1

First update of Goéland beta version.

• Now parses the whole TPTP FOF library (includes included, no pun intended).
• Removed plugins to make a statically linked binary. Added options to use plugins.
• Proof output.

v1.0.0-beta

This is the first release of Goéland, a concurrent automated theorem prover using tableau method for first order logic.

It :

• Proves theorems with TPTP files format (without include statements) ;
• Provides proofs in json format ;
• Includes polarized deduction modulo theory (which can be deactivated).