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

Norihiro Kamide

Titles

Abstract

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.

References

[1] A. Almukdad and D. Nelson, Constructible falsity and inexact predicates, Journal of Symbolic Logic 49 (1984), pp. 231–233.

[2] R. Dyckhoﬀ, Contraction-free sequent calculi for intuitionistic logic, Journal of Symbolic Logic 57 (1992), pp. 795–807.

[3] R. Dyckhoﬀ, and S. Negri, Admissibility of structural rules for contraction-free systems of intuitionistic logic, Journal of Symbolic Logic 65 (2000), pp. 1499–1515.

[4] R. Dyckhoﬀ, and S. Negri, Admissibility of structural rules for extensions of contraction-free sequent calculi, Logic Journal of the IGPL 9 (4) (2001), pp. 573– 580.

[5] Y. Gurevich, Intuitionistic logic with strong negation, Studia Logica 36 (1977), pp. 49–59.

[6] F. Joachimski and R. Matthes, Short proofs of normalization for the simply-typed λ-calculus, permutative conversions and G¨odel’s T, Archive for Mathematical Logic 42 (2003), 59–87. R. Matthes, Erratum, 2 pages, 2004.

[7] N. Kamide, Natural deduction systems for Nelson’s paraconsistent logic and its neighbors, Journal of Applied Non-Classical Logics 15 (4) (2005), pp. 405–435.

[8] E.G.K. L´opez-Escobar, em Refutability and elementary number theory, Indagationes Mathematicae 34 (1972), pp. 362–374.

[9] G. Mints, Gentzen-type systems and resolution rules. Part I. Propositional logic, Lecture Notes in Computer Science 417, pp. 198–231.

[10] S. Negri and J. von Plato, Structural proof theory, Cambridge University Press, 2001.

[11] D. Nelson, Constructible falsity, Journal of Symbolic Logic 14 (1949), pp. 16–26.

[12] S. P. Odintsov, The class of extensions of Nelson’s paraconsistent logic, Studia Logica 9 (4) (2005), pp. 573–580.

[13] S. P. Odintsov and H. Wansing, Inconsistency-tolerant description logic: motivation and basic systems, In V. Hendricks and J. Malinowski eds., Trends in Logic, 50 Years of Studia Logica, Kluwer Academic Publishers, 2003, pp. 301–335.

[14] D. Pearce, Reasonig with negative information, II: hard negation, strong negation and logic programs, Lecture Notes in Computer Science 619 (1992), pp. 63–79.

[15] D. Pearce and A. Valverde, A ﬁrst order nonmonotonic extension of constructive logic, Studia Logica 80 (2005), pp. 321–346.

[16] D. Prawitz, Natural deduction: a proof-theoretical study, Almqvist and Wiksell, Stockholm, 1965.

[17] G. Priest, Paraconsistent logic, in Handbook of Philosophical Logic, 2nd edition, vol. 6, edited by D. M. Gabbay and F. Guenthner, Kluwer Academic Publishers, 2002, pp. 287–393.

[18] W. Rautenberg, Klassische und nicht-klassische Aussagenlogik, Vieweg, Braunschweig, 1979.

[19] P. Schroeder-Heister, Generalized rules, direct negation, and deﬁnitional reﬂection, Proceedings of the 1st World Congress on Universal Logic (UNILOG 2005), 2 pages, 2005.

[20] A. M. Tamminga and K. Tanaka, A natural deduction system for ﬁrst degree entailment, Notre Dame Journal of Formal Logic 40 (2) (1999), 258–272.

[21] A. S. Troelstra and H. Schwichtenberg, Basic proof theory, Cambridge University Press, 1996.

[22] N.N. Vorob’ev, A constructive propositional calculus with strong negation (in Russian), Doklady Akademii Nauk SSR 85 (1952), pp. 465–468.

[23] G. Wagner, Logic programming with strong negation and inexact predicates, Journal of Logic and Computation 1 (6) (1991), pp. 835–859.

[24] H. Wansing, The logic of information structures, Lecture Notes in Artiﬁcial Intelligence 681 (1993), 163 pages.

Information

Information: Reports on Mathematical Logic, 2010, Number 45, pp. 3 - 21

Article type: Original article

Titles:

Polish:

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

English:

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

Authors

Norihiro Kamide

Teikyo University, Faculty of Science and Engineering, Department of Human Information Systems, Toyosatodai 1-1, Utsunomiya-shi, Tochigi 320-8551, Japan

Published at: 20.09.2010

Article status: Open

Licence: None

Percentage share of authors:

Norihiro Kamide (Author) - 100%

Article corrections:

-

Publication languages:

English

View count: 1657

Number of downloads: 1086

Pobierz pełny tekst

Titles

Abstract

References

Information

Authors