Arnon Avron ; Ori Lahav - On Constructive Connectives and Systems

lmcs:967 - Logical Methods in Computer Science, December 25, 2010, Volume 6, Issue 4 - https://doi.org/10.2168/LMCS-6(4:12)2010
On Constructive Connectives and SystemsArticle

Authors: Arnon Avron ; Ori Lahav ORCID

Canonical inference rules and canonical systems are defined in the framework of non-strict single-conclusion sequent systems, in which the succeedents of sequents can be empty. Important properties of this framework are investigated, and a general non-deterministic Kripke-style semantics is provided. This general semantics is then used to provide a constructive (and very natural), sufficient and necessary coherence criterion for the validity of the strong cut-elimination theorem in such a system. These results suggest new syntactic and semantic characterizations of basic constructive connectives.

https://doi.org/10.2168/LMCS-6(4:12)2010
Source: arXiv.org:1011.4384
Volume: Volume 6, Issue 4
Secondary volumes: Selected Papers of the 18th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2009)
Published on: December 25, 2010
Imported on: June 28, 2010
Keywords: Computer Science - Logic in Computer Science, F.4.1, I.2.3
Licence: arXiv.org - Non-exclusive license to distribute

Classifications

Mathematics Subject Classification 20201
Sources:
  • [1] zbMATH Open.

6 Documents citing this article

Share and export

Consultation statistics

This page has been seen 3659 times.
This article's PDF has been downloaded 580 times.