Automating and Computing Paraconsistent Reasoning: Contraction-Free, Resolution and Type Systems

• Authors: Norihiro Kamide
• Languages of publication: PL

Abstracts

PL

Firstly, a contraction-free sequent system G4np for Nelson’s paraconsistent 4-valued logic N4 is introduced by modifying and extending a contraction-free system G4ip for intuitionistic propositional logic. The structural rule elimination theorem for G4np can be shown by combining Dyckhoff and Negri’s result for G4ip and an existing embedding result for N4. Secondly, a resolution system Rnp for N4 is introduced by modifying an intuitionistic resolution system Rip, which is originally introduced by Mints and modified by Troelstra and Schwichtenberg. The equivalence between Rnp and G4np can be shown. Thirdly, a typed λ-calculus for N4 is introduced based on Prawitz’s natural deduction system for N4 via the Curry-Howard correspondence. The strong normalization theorem of this calculus can be proved by using Joachimski and Matthes’ proof method for intuitionistic typed λ-calculi with premutative conversions.

Keywords

PL

• Publisher: [unknown2]
• Journal: Reports on Mathematical Logic
• Year: 2010
• Volume: 45

Dates

published

2010

online

07 - 07 - 2015

Contributors

author

Norihiro Kamide