Combining proof-search and counter-model construction for deciding Gödel-Dummett logic
Résumé
We present an algorithm for deciding Gödel-Dummett logic. The originality of this algorithm comes from the combination of proof-search in sequent calculus, which reduces a sequent to a set of pseudo-atomic sequents, and counter-model construction of such pseudo-atomic sequents by a fixpoint computation. From an analysis of this construction, we deduce a new logical rule which provides shorter proofs than the previous rule of G4-LC. We also present a linear implementation of the counter-model generation algorithm for pseudo-atomic sequents.