Abstract | ||
---|---|---|
Canonical propositional Gentzen-type calculi are a natural class of systems which in addition to the standard axioms and structural rules have only logical rules where exactly one occurrence of a connective is introduced and no other connective is mentioned. Cut-elimination in such systems is fully characterized by a syntactic constructive criterion of coherence. In this paper we extend the theory of canonical systems to the considerably more general class of signed calculi . We show that the extended criterion of coherence fully characterizes only analytic cut-elimination in such calculi, while for characterizing strong and standard cut-elimination a stronger criterion of density is required. Modular semantics based on non-deterministic matrices are provided for every coherent canonical signed calculus. |
Year | DOI | Venue |
---|---|---|
2009 | 10.1007/978-3-540-92687-0_3 | LFCS |
Keywords | Field | DocType |
analytic cut-elimination,stronger criterion,signed calculus,canonical system,coherent canonical,standard axiom,natural class,general class,non-deterministic matrices,syntactic constructive criterion,extended criterion | Atomic formula,Analytic proof,Discrete mathematics,Combinatorics,Algebra,Matrix (mathematics),Axiom,Constructive,Natural class,Sequent calculus,Coherence (physics),Mathematics | Conference |
Volume | ISSN | Citations |
5407 | 0302-9743 | 4 |
PageRank | References | Authors |
0.52 | 9 | 2 |
Name | Order | Citations | PageRank |
---|---|---|---|
Arnon Avron | 1 | 1292 | 147.65 |
Anna Zamansky | 2 | 245 | 43.38 |