Skip to Main content Skip to Navigation

Preuves, réfutations et contre-modèles dans des logiques intuitionnistes

Abstract : Logics can be used as powerful tools for specifying computer systems and proving the soundness of their implementations with respect to these specifications. In the field of substructural logics, we develop tools and methods for automated deduction and counter-model generation. These logics involve the notion of resource : at the level of proof-search, the management of resources enables more efficient procedures : at the semantic level, resource models provide sound and complete interpretations. We develop a link between the syntactic notion of refutation and the semantic notion of counter-model. We deduce methods for proving the finite model property and algorithms for implementation of a proof-search procedure, based on a fine management of resources. In intuitionistic linear logic, resource based models constitute the core of an elegant proof of the finite model property. Furthermore, we establish a link between resource models and Petri net based models, from which we improve the proeceding partial completness results.
Document type :
File URL :
Complete list of metadata
Contributor : Thèses Ul <>
Submitted on : Thursday, March 29, 2018 - 10:39:19 AM
Last modification on : Thursday, January 7, 2021 - 11:49:38 AM


  • HAL Id : tel-01746507, version 1



Dominique Larchey-Wendling. Preuves, réfutations et contre-modèles dans des logiques intuitionnistes. Autre [cs.OH]. Université Henri Poincaré - Nancy 1, 2000. Français. ⟨NNT : 2000NAN10158⟩. ⟨tel-01746507⟩



Record views