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

• Autorzy: Alve G.V. , Oliveira A.G.,de , Queiroz R., de
• Języki publikacji: EN

Abstrakty

EN

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.

Słowa kluczowe

EN

proof theory; normalization procedure; proof-graphs; multiple conclusion; cycles

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2011
• Tom: Vol. 106, nr 2-4
• Strony: 119--147
• Opis fizyczny: Bibliogr. 15 poz.

Twórcy

autor

Alve G.V.

autor

Oliveira A.G.,de

autor

Queiroz R., de

• Centro de Informatica, Universidade Federal de Pernambuco, Av. Professor Luýs Freire s/n, Cidade Universitaria - Recife - PE - Brasil, CEP: 50740-540,

Bibliografia

• [1] Abramsky, S.: Proofs as Processes, Theoretical Computer Science, 135, 1994, 5-9.
• [2] Alves, G. V., de Oliveira, A. G., de Queiroz, R.: Transformations via Geometric Perspective Techniques Augmented with Cycles Normalization, 16th International Workshop on Logic, Languague, Information and Computation (H. Ono, M. Kanazawa, R. de Queiroz, Eds.), LNAI 5514, Springer, 2009.
• [3] Andou, Y.: A normalization-procedure for the first order classical natural deduction with full logical symbols, Tsukuba Journal of Mathematics, 19(1), 1995, 153-162.
• [4] Blute, R., Cockett, J. R. B., Seely, R. A. G., Trimble, T. H.: Natural Deduction and Coherence for Weakly Distributive Categories, Journal of Pure and Applied Algebra, 13(3), 1996, 229-296.
• [5] Buss, S. R.: The undecidability of k-provability, Annals of Pure and Applied Logic, 53(1), 8 July 1991, 75-102.
• [6] Carbone, A.: Duplication of Directed Graphs and Exponential Blow Up of Proofs, Ann. Pure Appl. Logic, 100(1-3), 1999, 1-67.
• [7] Cellucci, C.: Existential instantiation and normalization in sequent natural deduction, Annals of Pure and Applied Logic, 58(2), 28 September 1992, 111-148.
• [8] Guglielmi, A., Gundersen, T.: Normalisation Control in Deep Inference via Atomic Flows, Logical Methods in Computer Science, 4, 2008.
• [9] de Oliveira, A. G.: Proofs from a Geometric Perspective, Ph.D. Thesis, Centro de Inform´atica - Universidade Federal de Pernambuco, Abril 2001.
• [10] de Oliveira, A. G., de Queiroz, R. J. G. B.: Geometry of Deductions via Graphs of Proofs, chapter 1 of Logic for Concurrency and Synchronisation, Trends in Logic - Studia Logic Library, Kluwer Academic Publishers, July 2003, 1-86.
• [11] Pereira, L. C. P. D., Massi, C. D. B.: Normalizac¸ ˜ao para a l´ogica cl´assica, III Encontro Nacional de Filosofia, 1988, 5, Gramado, RS - Brasil.
• [12] Prawitz, D.: Ideas and Results in Proof Theory, in: Proceedings 2nd Scandinavian Logic Symp., Oslo, Norway, 18-20 June 1970 (J. E. Fenstad, Ed.), vol. 63 of Studies in Logic and the Foundations of Mathematics, North-Holland, Amsterdam, 1971, 235-307.
• [13] Stålmarck, G.: Normalization Theorems for Full First Order Classical Natural Deduction, Journal of Symbolic Logic, 56(1), 1991, 129-149.
• [14] Statman, R.: Structural Complexity of Proofs, Ph.D. Thesis, Stanford University, May 1974.
• [15] Ungar, A. M.: Normalization, Cut-Elimination and the Theory of Proofs, vol. 28 of CSLI Lecture Notes, CSLI Publications, Stanford, CA, 1992.