Citations of work:

Y. Andou (2003). Church–Rosser Property of a Simple Reduction for Full First-Order Classical Natural Deduction.

4 found
Order:
Are we missing citations?

PhilPapers citations & references are currently in beta testing. We expect to add many more in the future.

Meanwhile, you can use our bibliography tool to import references for this or another work.

Or you can directly add citations for the above work:

Search for work by author name and title
Add directly by record ID

  1.  2
    Some Properties of the-Calculus.Karim Nour & Khelifa Saber - 2012 - Journal of Applied Non-Classical Logics 22 (3):231-247.
    In this paper, we present the -calculus which at the typed level corresponds to the full classical propositional natural deduction system. The Church?Rosser property of this system is proved using the standardisation and the finiteness developments theorem. We also define the leftmost reduction and prove that it is a winning strategy.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  2.  3
    Strong Normalization of Classical Natural Deduction with Disjunctions.Koji Nakazawa & Makoto Tatsuta - 2008 - Annals of Pure and Applied Logic 153 (1-3):21-37.
    This paper proves the strong normalization of classical natural deduction with disjunction and permutative conversions, by using CPS-translation and augmentations. Using them, this paper also proves the strong normalization of classical natural deduction with general elimination rules for implication and conjunction, and their permutative conversions. This paper also proves that natural deduction can be embedded into natural deduction with general elimination rules, strictly preserving proof normalization.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  3.  8
    Non-Strictly Positive Fixed Points for Classical Natural Deduction.Ralph Matthes - 2005 - Annals of Pure and Applied Logic 133 (1):205-230.
    Termination for classical natural deduction is difficult in the presence of commuting/permutative conversions for disjunction. An approach based on reducibility candidates is presented that uses non-strictly positive inductive definitions.It covers second-order universal quantification and also the extension of the logic with fixed points of non-strictly positive operators, which appears to be a new result.Finally, the relation to Parigot’s strictly positive inductive definition of his set of reducibility candidates and to his notion of generalized reducibility candidates is explained.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   5 citations  
  4.  30
    A Short Proof of the Strong Normalization of Classical Natural Deduction with Disjunction.René David & Karim Nour - 2003 - Journal of Symbolic Logic 68 (4):1277-1288.
    We give a direct, purely arithmetical and elementary proof of the strong normalization of the cut-elimination procedure for full (i.e., in presence of all the usual connectives) classical natural deduction.
    Direct download (9 more)  
     
    Export citation  
     
    Bookmark   5 citations