Banca Examinadora: Kátia Silva Guimarães (CIn-UFPE), José Dias dos Santos (CIn-UFPE), Marcelo Finger (DCC/IME-USP), Luiz Carlos Pereira (Filosofia/PUC-Rio), Antônio Carlos da Rocha Costa (UCPel).
Orientador: Ruy J. G. B. de Queiroz
(Durante a elaboração deste trabalho, o autor recebeu apoio financeiro da CAPES)
(Para obter o arquivo postscript com o texto integral clique aqui)
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.