Combining proof-search and counter-model construction for deciding Gödel-Dummett logic
Dominique Larchey-Wendling, Loria Universite · 2002
Abstract. 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 construc-tion, we deduce a new logical rule [⊃N] which provides shorter proofs than the rule [⊃R] of G4-LC. We also present a linear implementation of the counter-model generation algorithm for pseudo-atomic sequents. 1