Tools

Goéland

Work done in collaboration with David Delahaye, Isaac Lluís and Johann Rosain.

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.

Please refer to this paper if you want to cite SC-TPTP utilities:

@inproceedings{cailler2024sc,
  title={SC-TPTP: An Extension of the TPTP Derivation Format for Sequent-Based Calculus},
  author={Cailler, Julie and Guilloud, Simon},
  booktitle={9th Workshop on Practical Aspects of Automated Reasoning},
  year={2024}
}

LastButNotLeast

The fastest way to give up — now with 0 bugs! Probably the fastest prover in the competition:

Runs flawlessly.
Achieves absolutely nothing.
100% success rate in failure.
Zero proof, infinite potential.
Proudly earns you a cool CASC T-shirt.

Unfortunately, designing this prover may force you to share a meal with very weird people — but hey, that’s the price of true innovation.

The strategy is simple: always return GaveUp. It’s fast, reliable, and guarantees we never solve anything — by design.

The prover is expected to come last at CASC competition, and any other result would be genuinely surprising — possibly even concerning. In fact, LastButNotLeast proudly exists to ensure that no other prover — no matter how underwhelming — has to carry the burden of being last.

Implementation

#!/usr/bin/env python

print("% LastButNotLeast: The fastest way to give up!")
print("% For best results, do not expect results.")
print("% SZS status GaveUp")
print("% It's not a bug - it's a philosophical stance.")
print("% Thanks for trying LastButNotLeast :)")