Name
Abstract | ||
|---|---|---|
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. |
Year | DOI | Venue |
|---|---|---|
2010 | 10.2168/LMCS-6(4:12)2010 | LOGICAL METHODS IN COMPUTER SCIENCE |
Keywords | Field | DocType |
sequent calculus,cut-elimination,nonclassical logics,non-deterministic semantics,Kripke semantics | Proof-theoretic semantics,Discrete mathematics,Constructive,Coherence (physics),Sequent,Rule of inference,General semantics,Syntax,Semantics,Mathematics | Journal |
Volume | Issue | ISSN |
6 | 4 | 1860-5974 |
Citations | PageRank | References |
7 | 0.69 | 4 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Arnon Avron | 1 | 1292 | 147.65 |
| Ori Lahav | 2 | 252 | 23.53 |