Combining proof-search and linear counter-model construction

Colloque sur invitation. internationale.International audienceIn this talk, we present a proof-search algorithm that integrates a counter-model generation method based on the computation of semantic fixpoints. It is dedicated to Gödel-Dummett Logic, that is a so-called intermediate logic with linear Kripke models, but we aim to apply similar techniques, based on combination of proof and countermodel searchs, to other ressources logics. Reference counting techniques are central for an efficient implementation of those fixpoint computations