Download PDFOpen PDF in browser

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

EasyChair Preprint 8676

10 pagesDate: August 12, 2022

Abstract

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.

Keyphrases: automated theorem proving, concurrency, tableaux

BibTeX entry
BibTeX does not have the right entry for preprints. This is a hack for producing the correct reference:
@booklet{EasyChair:8676,
  author    = {Julie Cailler and Johann Rosain and David Delahaye and Simon Robillard and Hinde Bouziane},
  title     = {Goéland: a Concurrent Tableau-Based Theorem Prover (System Description)},
  howpublished = {EasyChair Preprint 8676},
  year      = {EasyChair, 2022}}
Download PDFOpen PDF in browser