Линейная логика (англ. linear logic) — подструктурная логика, предложенная Жан-Ивом Жираром[англ.] как уточнение классической и интуиционистской логики, объединяющая двойственность первой со многими конструктивными свойствами последней[1], введена и используется для логических рассуждений, учитывающих расход некоторого ресурса[2]. Хотя логика также изучалась сама по себе, идеи линейной логики находят применения во множестве приложений, вычисления в которых требуют учёта ресурсов, в том числе для верификации сетевых протоколов, языки программирования, теория игр (игровая семантика)[2] и квантовая физика (поскольку линейную логику можно рассматривать как логику квантовой теории информации)[3], лингвистика[4].
Язык классической линейной логики (англ. classic linear logic, CLL) может быть описан в форме Бэкуса — Наура:
Каждое утверждение A в классической линейной логике имеет двойственное A⊥, определяемое следующим образом:
В линейной логике (в отличие от классической) посылки часто рассматриваются как расходуемые ресурсы, поэтому выведенная или начальная формула может быть ограничена по числу использований.
Мультипликативная конъюнкция ⊗ аналогична операции сложения мультимножеств и может выражать объединение ресурсов.
Следует отметить, что (.)⊥ является инволюцией, то есть, A⊥⊥ = A для всех утверждений. A⊥ также называется линейным отрицанием A.