Natural deduction systems for some non-commutative logics
DOI:
https://doi.org/10.12775/LLP.2007.005Keywords
constructive sequential propositional logic (COSPL), full Lambek logic (FL), natural deduction, (strong) normalizationAbstract
Varieties of natural deduction systems are introduced for Wansing’s paraconsistent non-commutative substructural logic, called a constructive sequential propositional logic (COSPL), and its fragments. Normalization, strong normalization and Church-Rosser theorems are proved for these systems. These results include some new results on full Lambek logic (FL) and its fragments, because FL is a fragment of COSPL.References
van Benthem, J., Language in action — categories, lambdas and dynamic logic, Elsevier Science Publishers, 1991.
Gabbay D.M., and Ruy. J.G.B. de Queiroz, “Extending the Curry-Howard interpretation to linear, relevant and other resource logics”, Journal of Symbolic Logic 57 (4), 1319–1365, 1992.
Hindley, J.R., “BCK-combinators and linear ?-term have types”, Theoretical Computer Science 64, 97–105, 1986.
Kamide, N., “Natural deduction systems for Nelson’s paraconsistent logic and its neighbors”, Journal of Applied Non-Classical Logics 15 (4), 405–435, 2005.
Mouri, M., A proof-theoretic study of non-classical logics — natural deduction systems for intuitionistic substructural logics and implemetation of proof assistant system. (in Japanese). Doctoral dissertation, Japan Advanced Institute of Science and Technology, 2002.
Negri, S., “A normalizing system of natural deduction for intuitionistic linear logic”, Archive for Mathematical Logic 41, 789–810, 2002.
Negri, S., “Varieties of linear calculi”, Journal of Philosophical Logic 31, 569–590, 2002.
Negri, S., and J. von Plato, “Sequent calculus in natural deduction style”, Journal of Symbolic Logic 66 (4), 1803–1816, 2001.
Nelson, D., Constructible falsity. Journal of Symbolic Logic 14, 16–26, 1949.
Polakow, J., and F. Pfenning, “Natural deduction for intuitionistic non-commutative linear logic”, Lecture Notes in Computer Science 1581, 295–309, 1999.
Priest, G., and R. Routley, “Introduction: paraconsistent logics”, Studia Logica 43, 3–16, 1982.
Tiede, H.-J., “Proof theory and formal grammars — applications of normalization”, in T. Raesch et al. (eds.), Foundations of the Formal Sciences II: Applications of Mathematical Logic in Philosophy and Linguistics, Kluwer Academic Publishers, 2003.
Wagner, G., “Logic programmingwith strong negation and inexact predicates”, Journal of Logic and Computation 1 (6), 835–859, 1991.
Wansing, H., “Formulas-as-types for a hierarchy of sublogics of intuitionistic propositional logic”, Lecture Notes in Artificial Intelligence 619, 125–145, 1990.
Wansing, H., The logic of information structures, Lecture Notes in Artificial Intelligence 681, 1993, 163 pages.
Watari, O., K. Nakatogawa, and T. Ueno, “Normalization theorems for sub-structural logics in Gentzen-style natural deduction (abstract)”, Bulletin of Symbolic Logic 6 (3), 390–391, 2000.
Downloads
Published
How to Cite
Issue
Section
Stats
Number of views and downloads: 718
Number of citations: 0
