Skip to Main content Skip to Navigation
Theses

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 :
Theses
File URL :
http://docnum.univ-lorraine.fr/prive/SCD_T_2004_0160_MERY.pdf
Complete list of metadatas

https://hal.univ-lorraine.fr/tel-01746770
Contributor : Thèses Ul <>
Submitted on : Thursday, March 29, 2018 - 10:44:33 AM
Last modification on : Tuesday, September 1, 2020 - 3:14:28 PM

Identifiers

  • HAL Id : tel-01746770, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

17