Goéland - LIRMM - Laboratoire d’Informatique, de Robotique et de Microélectronique de Montpellier Accéder directement au contenu
Logiciel Année : 2022

Goéland

Julie Cailler
Johann Rosain
David Delahaye

Résumé

Goéland is an automated theorem prover for first-order logic that relies on a concurrent search procedure to find tableau proofs, with concurrent processes corresponding to individual branches of the tableau. Since branch closure may require instantiating free variables shared across branches, processes communicate via channels to exchange information about substitutions used for closure. We present the proof-search procedure and its implementation, as well as experimental results obtained on problems from the TPTP library.
169 Consultations
10 Téléchargements

Partager

Gmail Mastodon Facebook X LinkedIn More