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 :
Theses
Complete list of metadatas

Cited literature [1 references]  Display  Hide  Download

https://hal.univ-lorraine.fr/tel-01749530
Contributor : Thèses Ul <>
Submitted on : Thursday, March 29, 2018 - 12:18:49 PM
Last modification on : Tuesday, April 24, 2018 - 1:31:01 PM
Long-term archiving on : Friday, September 14, 2018 - 9:54:56 AM

File

INPL_2011_NOVAKOVIC_N.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : tel-01749530, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

22

Files downloads

13