PL EN


Preferences help
enabled [disable] Abstract
Number of results
2010 | 45 |
Article title

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

Authors
Content
Title variants
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
Year
Volume
45
Physical description
Dates
published
2010
online
07 - 07 - 2015
Contributors
References
Document Type
Publication order reference
Identifiers
YADDA identifier
bwmeta1.element.ojs-issn-2084-2589-year-2010-volume-45-article-2862
JavaScript is turned off in your web browser. Turn it on to take full advantage of this site, then refresh the page.