## Mechanizing Proof Theory: Resource-Aware Logics and
Proof-Transformations to extract implicit information

**G Bellin**
*Abstract:* 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 inly 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
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*
(sections 3 and 4) and an extension of Direct Logic of interest for
nonmonotonic reasoning (section 8). In Part II we study Herbrand's
Theorem in Linear Logic and the No Counterexample Interpretation in
a fragment of Peano Arithmetic (section 10). 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 (sections
10-13).

**PhD Thesis - Price £8.50**

*LFCS report ECS-LFCS-91-165 (also published as
CST-80-91)*

Previous |

Index |

Next