Skip to Main content Skip to Navigation
Conference papers

Combining proof-search and linear counter-model construction

Dominique Larchey-Wendling 1
1 TYPES - Logic, proof Theory and Programming
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : In 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.
Document type :
Conference papers
Complete list of metadata
Contributor : Publications Loria <>
Submitted on : Tuesday, September 26, 2006 - 9:38:40 AM
Last modification on : Friday, February 26, 2021 - 3:28:08 PM


  • HAL Id : inria-00099553, version 1



Dominique Larchey-Wendling. Combining proof-search and linear counter-model construction. First APPSEM-II Workshop 2003 - (Applied Semantics II), 2003, Nottingham/UK. ⟨inria-00099553⟩



Record views