Demostramos un teorema de linealidad para una extensión de la lógica lineal con adición y multiplicación por un escalar: las pruebas de algunas proposiciones en esta lógica son lineales en el sentido algebraico. Este trabajo forma parte de un programa de investigación más amplio que tiene como objetivo definir una lógica cuyo lenguaje de prueba sea un lenguaje de programación cuántica.

Nous prouvons un théorème de linéarité pour une extension de la logique linéaire avec addition et multiplication par un scalaire : les preuves de certaines propositions dans cette logique sont linéaires au sens algébrique. Ce travail s'inscrit dans un programme de recherche plus large qui vise à définir une logique dont le langage de preuve est un langage de programmation quantique.

We prove a linearity theorem for an extension of linear logic with addition and multiplication by a scalar: the proofs of some propositions in this logic are linear in the algebraic sense. This work is part of a wider research program that aims at defining a logic whose proof language is a quantum programming language.

نثبت نظرية خطية لتمديد المنطق الخطي مع الجمع والضرب في عدد قياسي: إن براهين بعض الافتراضات في هذا المنطق خطية بالمعنى الجبري. هذا العمل هو جزء من برنامج بحثي أوسع يهدف إلى تحديد المنطق الذي تكون لغته الإثباتية هي لغة البرمجة الكمومية.