CINECA IRIS Institutional Research Information System
IRIS è l'Anagrafe della ricerca dell'Università degli Studi di Trento, e ha lo scopo di raccogliere, documentare, conservare e diffondere, anche ad accesso aperto, la produzione scientifica degli autori afferenti all'Università degli Studi di Trento.
EnglishThe calculus of structures is a proof theoretical formalism which generalizes the sequent calculus with the feature of deep inference: In contrast to the sequent calculus, inference rules can be applied at any depth inside a formula, bringing shorter proofs than any other formalisms supporting analytical proofs. However, deep applicability of the inference rules causes greater nondeterminism than in the sequent calculus regarding proof search. In this paper, we introduce a new technique which reduces nondeterminism without breaking proof theoretical properties and provides a more immediate access to shorter proofs. We present this technique on system BV, the smallest technically non-trivial system in the calculus of structures, extending multiplicative linear logic with the rules mix, nullary mix, and a self-dual non-commutative logical operator. Because our technique exploits a scheme common to all the systems in the calculus of structures, we argue that it generalizes to these systems for classical logic, linear logic, and modal logics.
Scheda prodotto non validato
I dati visualizzati non sono stati ancora sottoposti a validazione formale da parte dello Staff di IRIS, ma sono stati ugualmente trasmessi al Sito Docente Cineca (Loginmiur).
| Titolo: | Reducing Nondeterminism in the Calculus of Structures |
| Autori: | Kahramanogullari, Ozan |
| Autori Unitn: | |
| Titolo del volume contenente il saggio: | Logic for Programming, Artificial Intelligence, and Reasoning, 13th International Conference, LPAR 2006, Phnom Penh, Cambodia, November 13-17, 2006, Proceedings. |
| Luogo di edizione: | Berlin |
| Casa editrice: | Springer-Verlag |
| Anno di pubblicazione: | 2006 |
| Codice identificativo Scopus: | 2-s2.0-33845216234 |
| Codice identificativo ISI: | WOS:000243118200019 |
| ISBN: | 3540482814 |
| Handle: | http://hdl.handle.net/11572/99931 |
| Appare nelle tipologie: | 04.1 Saggio in atti di convegno (Paper in proceedings) |
File in questo prodotto:
http://hdl.handle.net/11572/99931
Copyright © 2020