Affiliations: Centro de Informática, Universidade Federal de Pernambuco, Recife, Brazil. gva@cin.ufpe.br; ago@cin.ufpe.br; ruy@cin.ufpe.br
Note: [] Thanks for the support of FACEPE/CAPES (Brazilian Federal Research Agency) by means of the doctoral scholarship. Address for correspondence: Centro de Informática, Universidade Federal de Pernambuco, Av. Professor Luís Freire s/n, Cidade Universitária - Recife - PE - Brasil, CEP: 50740-540
Abstract: A normalization procedure is presented for a classical natural deduction (ND) proof system. This proof system, called N-Graphs, has a multiple conclusion proof structure, where cycles are allowed. With this, we have developed a thorough treatment of cycles, including cycles normalization via an algorithm. We also demonstrate the usefulness of the graphical framework of N-Graphs, where derivations are seen as digraphs. We use geometric perspective techniques to establish the normalization mechanism, thus giving a direct normalization proof. Moreover, the subformula and separation properties are determined.
