Goéland: A Concurrent Tableau-Based Theorem Prover (System Description) - LIRMM - Laboratoire d’Informatique, de Robotique et de Microélectronique de Montpellier Accéder directement au contenu
Communication Dans Un Congrès Année : 2022

Goéland: A Concurrent Tableau-Based Theorem Prover (System Description)

Résumé

We describe Goéland, 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.
Fichier principal
Vignette du fichier
Goéland22.pdf (387.69 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

lirmm-03793406 , version 1 (01-10-2022)

Licence

Paternité

Identifiants

Citer

Julie Cailler, Johann Rosain, David Delahaye, Simon Robillard, Hinde Lilia Bouziane. Goéland: A Concurrent Tableau-Based Theorem Prover (System Description). IJCAR 2022 - 11th International Joint Conference on Automated Reasoning, Aug 2022, Haifa, Israel. pp.359-368, ⟨10.1007/978-3-031-10769-6_22⟩. ⟨lirmm-03793406⟩
116 Consultations
93 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More