Proof-graphs: a Thorough Cycle Treatment, Normalization and Subformula Property

Issue title: Logic, Language, Information and Computation

Article type: Research Article

Authors: Alves, Gleifer V. | de Oliveira, Anjolina G. | de Queiroz, Ruy

Affiliations: Centro de Informática, Universidade Federal de Pernambuco, Recife, Brazil. [email protected]; [email protected]; [email protected]

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.

Keywords: proof theory, normalization, proof-graphs, multiple conclusion, cycles

DOI: 10.3233/FI-2011-380

Journal: Fundamenta Informaticae, vol. 106, no. 2-4, pp. 119-147, 2011