| HAL-Inria | Publications, software ... of Inria's scientists |
Journal articles
On Proof Normalization in Linear Logic
Abstract : We present a proof-theoretic foundation for automated deduction in linear logic. At first, we systematically study the permutability properties of the
inference rules in this logical framework and exploit these to introduce an appropriate notion of forward and backward movement of an inference in a
proof. Then we discuss the naturally-arising question of the redundancy reduction and investigate the definition of the normal proof concept.
We briefly consider some of the issues related to proof construction mechanization in linear logic and to the design of logic programming languages from linear logic fragments.
Keywords :
Linear Logic
Proof Theory
https://hal.inria.fr/hal-01297755
Contributor : Guy Perrier <>
Submitted on : Monday, April 4, 2016 - 5:42:32 PM
Last modification on : Wednesday, May 12, 2021 - 4:56:04 PM
Long-term archiving on: : Monday, November 14, 2016 - 3:59:00 PM
Contributor : Guy Perrier <>
Submitted on : Monday, April 4, 2016 - 5:42:32 PM
Last modification on : Wednesday, May 12, 2021 - 4:56:04 PM
Long-term archiving on: : Monday, November 14, 2016 - 3:59:00 PM
File
tcs1994.pdf
Files produced by the author(s)