Linear logic as a framework for specifying sequent calculus
Dale Armin Miller, Elaine Gouvêa Pimentel · Cambridge University Press eBooks · 2017
. In recent years, intuitionistic logic and type systems have been used in numerous computational logic systems as frameworks for the specification of natural deduction proof systems. As we shall illustrate here, linear logic can be similarly used to specify the more general setting of sequent calculus proof systems. We shall present several example encodings of sequent calculus proof system using the Forum presentation of linear logic. x1. Overview of Linear Logic and Forum. Linear Logic [9] uses the following logical connectives: the exponentials ! and ?;\\Omega , . . . . . .. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . ........ , ?, and 1 for the multiplicative conjunction, disjunction, false, and true; &, \\Phi, 0, ? for the additive version of these connectives; \\Gammaffi for linear implication, and 8 and 9 for universal and existential quantification. We sha...