Skip to Main content Skip to Navigation
New interface

Sémantique algébrique des ressources pour la logique classique

Abstract : The general theme of this thesis is the exploitation of the fruitful interaction between denotational semantics and syntax. Satisfying semantics have been discovered for proofs in intuitionistic and certain linear logics, but for the classical case, solving the problem is notoriously difficult.This work begins with investigations of concrete interpretations of classical proofs in the category of posets and bimodules, resulting in the definition of meaningful invariants of proofs. Then, generalizing this concrete semantics, classical proofs are interpreted in a free symmetric compact closed category where each object is endowed with the structure of a Frobenius algebra. The generalization paves a way for a theory of proof nets for classical proofs. Correctness, cut elimination and the issue of full completeness are addressed through natural order enrichments defined on the Frobenius category, yielding a category with cut elimination and a concept of resources in classical logic. Revisiting our initial concrete semantics, we show we have a faithful representation of the Frobenius category in the category of posets and bimodules.
Document type :
Complete list of metadata

Cited literature [1 references]  Display  Hide  Download
Contributor : Thèses UL Connect in order to contact the contributor
Submitted on : Thursday, March 29, 2018 - 12:18:49 PM
Last modification on : Saturday, October 16, 2021 - 11:26:08 AM
Long-term archiving on: : Friday, September 14, 2018 - 9:54:56 AM


Files produced by the author(s)


  • HAL Id : tel-01749530, version 1



Novak Novakovic. Sémantique algébrique des ressources pour la logique classique. Autre [cs.OH]. Institut National Polytechnique de Lorraine, 2011. Français. ⟨NNT : 2011INPL075N⟩. ⟨tel-01749530⟩



Record views


Files downloads