Линейная логика

Линейная логика (англ. Linear Logic — это подструктурная логика, предложенная (англ. Jean-Yves Girard) как уточнение классической и интуиционистской логики, объединяющая двойственность первой со многими конструктивными свойствами последней, введена и используется для логических рассуждений, учитывающих расход некоторого ресурса. Хотя логика также изучалась сама по себе, идеи линейной логики находят применения во множестве приложений, вычисления в которых требуют учёта ресурсов, в том числе для верификации сетевых протоколов, языки программирования, теория игр и квантовая физика (поскольку линейную логику можно рассматривать как логику квантовой теории информации), лингвистика.