Automating and computing paraconsistent reasoning: contraction-free, resolution and type systems

• Autorzy: Kamide N.
• Języki publikacji: EN

Abstrakty

EN

Firstly, a contraction-free sequent system G4np for Nelson’s paraconsistent 4-valued logic N4 is introduced by modify- ing 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 in- tuitionistic 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 lambda-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 lambda-calculi with premutative conversions.

• Wydawca: Wydawnictwo Uniwersytetu Jagiellońskiego
• Czasopismo: Reports on Mathematical Logic
• Rocznik: 2010
• Tom: Vol. 45
• Strony: 3--21
• Opis fizyczny: Bibliogr. 24 poz.

Twórcy

autor

Kamide N.

• Waseda Institute for Advanced Study, 1-6-1 Nishi Waseda, Shinjuku-ku, Tokyo 169-8050, JAPAN,

Bibliografia

• [1] A. Almukdad and D. Nelson, Constructible falsity and inexact predicates, Journal of Symbolic Logic 49 (1984), pp. 231–233.
• [2] R. Dyckhoff, Contraction-free sequent calculi for intuitionistic logic, Journal of Sym-bolic Logic 57 (1992), pp. 795–807.
• [3] R. Dyckhoff, 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. Dyckhoff, 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 lambda-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 first 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, Braun-schweig, 1979.
• [19] P. Schroeder-Heister, Generalized rules, direct negation, and definitional reflection,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 first 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 Artificial Intelligence 681 (1993), 163 pages.