PL EN


Preferencje help
Widoczny [Schowaj] Abstrakt
Liczba wyników
Tytuł artykułu

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

Wybrane pełne teksty z tego czasopisma
Identyfikatory
Warianty tytułu
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.
Wydawca
Rocznik
Strony
119--147
Opis fizyczny
Bibliogr. 15 poz.
Twórcy
autor
  • Centro de Informatica, Universidade Federal de Pernambuco, Av. Professor Luýs Freire s/n, Cidade Universitaria - Recife - PE - Brasil, CEP: 50740-540, gva@cin.ufpe.br
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.
Typ dokumentu
Bibliografia
Identyfikator YADDA
bwmeta1.element.baztech-article-BUS8-0012-0062
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.