Les reseaux de preuve de la Logique Lineaire (LL)
ont parmi leurs ambitions celle de fournir une representation du contenu
calculatoire des demonstrations.
Une facon de tester la "qualite" de cette representation est de se
demander si on peut operer "plus d'identifications" que ne font les
reseaux. Ceci conduit tout naturellement a` se demander si les modeles
(denotationnels) de LL sont en mesure d'identifier deux reseaux
"syntaxiquement differents": nous dirons d'un modele qu'il est
"injectif" lorsqu'il ne permet pas de telles identifications.
Nous poserons avec precision la question de l'injectivite, et nous
exposerons quelques resultats pour le modele coherent et
pour le modele relationnel de LL. Nous retrouverons lors de cette analyse
deux questions a` la mode en ce moment: celle de la
"polarisation/focalisation" des preuves de LL, et celle
de l'"uniformite" de la semantique.