Tools

Goéland

Goéland is an automated theorem prover for first-order logic with equality. It relies on a concurrent proof-search procedure based on the method of free-variable analytics tableaux that allows it to perform a fair branch exploration. The prover is also able to deal with axiomatisable theories thanks to a module of deduction modulo theory, to deal with polymorphic types, and to produce machine-checkable proofs in Coq, Lambdapi and Lisa.

Please refer to this paper if you want to cite Goéland.

@inproceedings{cailler2022goeland,
  author       = {Julie Cailler and
                  Johann Rosain and
                  David Delahaye and
                  Simon Robillard and
                  Hinde Lilia Bouziane},
  editor       = {Jasmin Blanchette and
                  Laura Kov{\'{a}}cs and
                  Dirk Pattinson},
  title        = {Go{\'{e}}land: {A} Concurrent Tableau-Based Theorem Prove (System Description)},
  booktitle    = {Automated Reasoning - 11th International Joint Conference, {IJCAR} 2022, Haifa, Israel, August 8-10, 2022, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {13385},
  pages        = {359--368},
  publisher    = {Springer},
  year         = {2022},
  url          = {https://doi.org/10.1007/978-3-031-10769-6\_22},
  doi          = {10.1007/978-3-031-10769-6\_22}
}

SC-TPTP Utilities

Work done in collaboration with Simon Guilloud.

SC-TPTP Utilities is a library of tools able to deal with the SC-TPTP format. It includes softwares able to handle, import, export and transform proofs in SC-TPTP format, to add intermediate proof steps, and to export them into Coq.