(**Para obter o arquivo postscript com o texto integral clique aqui**)

## Abstract

We are here concerned with the study of proofs from a geometric perspective.
By first recalling the pioneering work of Statman in proposing such kind of
study in his doctoral thesis *Structural Complexity of Proofs* (1974),
we review two recent research programmes which approach the study of
structural properties of formal proofs from a geometric perspective:
(i) the notion of *proof-net*, given by Girard in 1987 in the context
of linear logic; and (ii) the notion of *logical flow graph* given by
Buss in 1991 and used as a tool for studying the exponential blow up of proof
sizes caused by the cut-elimination process, a very recent programme
(1996-2000) proposed by Carbone in collaboration with Semmes.
We consider these two works as our
starting point in the investigation of proofs from a geometric perspective,
and they shall guide the formulation of our present proposal.
Statman's geometric perspective does not seem to have developed
much further than his doctoral thesis, but the fact is that it looks as
if the main idea, *i.e.* extracting structural properties of proofs in
natural deduction using appropriate geometric intuitions, offers itself
as a very promising one. With this in mind, and having at our disposal some
interesting and rather novel techniques developed for *proof-nets* and
*logical flow graphs*, we have tried to focus our
investigation on a research for an alternative proposal for looking at the
geometry of natural deduction systems.
The lack of symmetry in natural deduction systems is one of the aspects
which represents a challenge for such a kind of study. Of course, one
alternative to deal with the problem of lack of symmetry in ND systems is
to look at multiple-conclusion calculi. We already have in the literature
different approaches involving such calculi. For example,
Kneale's (1958) *tables of development* (studied in depth by
Shoesmith and Smiley (1978)) and Ungar's (1992) multiple-conclusion natural
deduction.
Our proposal is similar to both Kneale's and Ungar's in various aspects,
mainly in the presentation of a multiple conclusion calculus inspired in
natural deduction systems. However, we wish to bring our system, which we
have named as **n-graphs**, into the current state-of-affairs by
incorporating some of the techniques developed for *proof-nets*
(*e.g.*, *splitting theorem*, *soundness criteria*, *sequentialization*), and at
the same time study its structural properties via a geometrical
representation of of proofs.
A future development should also include the study of the complexity of
ND derivations in the lines of the work of Carbone for the sequent
calculus.

*Última
atualização: 18 de Dezembro de 2001, 11:42:40 GMT-0200.*