Non-commutative logic III: focusing proofs
| Autor: | Roberto Maieli, Paul Ruet |
|---|---|
| Přispěvatelé: | Maieli, Roberto, Ruet, Paul |
| Rok vydání: | 2003 |
| Předmět: |
Discrete mathematics
sequent calculi Natural deduction Cut-elimination theorem Noncommutative logic Astrophysics::Instrumentation and Methods for Astrophysics proof theory Linear logic Computer Science Applications Theoretical Computer Science Algebra TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Computational Theory and Mathematics Proof calculus Focalization Proof theory Computer Science::Logic in Computer Science non commutative logic Sequent Information Systems Mathematics |
| Zdroj: | Information and Computation. 185:233-262 |
| ISSN: | 0890-5401 |
| Popis: | It is now well-established that the so-called focalization property plays a central role in the design of programming languages based on proof search, and more generally in the proof theory of linear logic. We present here a sequent calculus for non-commutative logic (NL) which enjoys the focalization property. In the multiplicative case, we give a focalized sequentialization theorem, and in the general case, we show that our focalized sequent calculus is equivalent to the original one by studying the permutabilities of rules for NL and showing that all permutabilities of linear logic involved in focalization can be lifted to NL permutabilities. These results are based on a study of the partitions of partially ordered sets modulo entropy. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full Text from ScienceDirect