This text is an outgrowth of notes prepared by J. Y. Girard for a course at the University of Paris VII. It deals with the mathematical background of the application to computer science of aspects of logic (namely the correspondence between proposition & types). Combined with the conceptual perspectives of Girard's ideas, this sheds light on both the traditional logic material & its prospective applications to computer science. The book covers a very active & exciting research area, & it will (...) be essential reading for all those working in logic & computer science. (shrink)

Linear logic, introduced by Girard, is a refinement of classical logic with a natural, intrinsic accounting of resources. This accounting is made possible by removing the ‘structural’ rules of contraction and weakening, adding a modal operator and adding finer versions of the propositional connectives. Linear logic has fundamental logical interest and applications to computer science, particularly to Petri nets, concurrency, storage allocation, garbage collection and the control structure of logic programs. In addition, there is a direct correspondence between polynomial-time computation (...) and proof normalization in a bounded form of linear logic. In this paper we show that unlike most other propositional logics, full propositional linear logic is undecidable. Further, we prove that without the modal storage operator, which indicates unboundedness of resources, the decision problem becomes PSPACE-complete. We also establish membership in NP for the multiplicative fragment, NP-completeness for the multiplicative fragment extended with unrestricted weakening, and undecidability for fragments of noncommutative propositional linear logic. (shrink)

Linear logic is a new logic which was recently developed by Girard in order to provide a logical basis for the study of parallelism. It is described and investigated in Gi]. Girard's presentation of his logic is not so standard. In this paper we shall provide more standard proof systems and semantics. We shall also extend part of Girard's results by investigating the consequence relations associated with Linear Logic and by proving corresponding str ong completeness theorems. Finally, we shall investigate (...) the relation between Linear Logic and previously known systems, especially Relevance logics. (shrink)

Few systems for mechanical proof-checking have been used so far to transform formal proofs rather than to formalize informal arguments and to verify correctness. The unwinding of proofs, namely, the process of applying lemmata and extracting explicit values for the parameters within a proof, is an obvious candidate for mechanization. It corresponds to the procedures of Cut-elimination and functional interpretation in proof-theory and allows the extraction of the constructive content of a proof, sometimes yielding information useful in mathematics and in (...) computing. ;Resource-aware logics restrict the number of times an assumption may be used in a proof and are of interest for proof-checking not only in relation to their decidability or computational complexity, but also because they efficiently solve the practical problem of representing the structure of relevance in a derivation. In particular, in Direct Logic only one subformula-occurrence of the input is allowed, and the connections established during a successful proof-verification can be represented on the input without altering it. In addition, the values for the parameters obtained from unwinding are read off directly. ;In Linear Logic, where classical logic is regarded as the limit of a resource-aware logic, long-standing issues in proof-theory have been successfully attacked. We are particularly interested in the system of proof-nets as a a multiple-conclusion Natural Deduction system for Linear Logic. ;In Part I of this thesis we present a new set of tools that provide a systematic and uniform approach to different resource-aware logics. In particular, we obtain uniqueness of the normal form for Multiplicative and Additive Linear Logic and an extension of Direct Logic of interest for nonmonotonic reasoning . In Part II we study Herbrand's Theorem in Linear Logic and the No Counterexample Interpretation in a fragment of Peano Arithmetic . As an application to Ramsey Theory we give a parametric form of the Ramsey Theorem, that generalizes the Infinite, the Finite and the Ramsey-Paris-Harrington Theorems for a fixed exponent. (shrink)