Skip to Main content Skip to Navigation
New interface

Preuves et sémantiques dans des logiques de ressources

Abstract : Resource-aware logics are powerful tools for specifying properties. In the context of a mathematical theory of resources, we build proof-search methods which capture the dynamic interactions between resources by means of labels and constraints. We present the BI-logic which, due to its resource-sharing interpretation, appears as the logical kernel of a wide range of resource logics. We develop tableau-based and connection-based proof-search methods, with counter-model generation facilities, for the consistent fragment of BI. We extend our proof methods to the whole fragment of propositional BI, showing that it is decidable and has the finite model property. We propose new complete semantics for BI and specialize ou methods to intuitionistic logic and intuitionistic multiplicative linear logic. We study the affine and boolean variants of BI and their links with the pointer logic.
Document type :
Complete list of metadata
Contributor : Thèses UL Connect in order to contact the contributor
Submitted on : Thursday, March 29, 2018 - 10:44:33 AM
Last modification on : Monday, February 7, 2022 - 10:04:06 AM

Intranet access


  • HAL Id : tel-01746770, version 1



Daniel Méry. Preuves et sémantiques dans des logiques de ressources. Autre [cs.OH]. Université Henri Poincaré - Nancy 1, 2004. Français. ⟨NNT : 2004NAN10160⟩. ⟨tel-01746770⟩



Record views