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.
EnglishSystem BV is an extension of multiplicative linear logic with a non-commutative self-dual operator. In this paper we present systems equivalent to system BV where equalities for unit are oriented from left to right and new structural rules are introduced to preserve completeness. While the first system allows units to appear in the structures, the second system makes it possible to completely remove the units from the language of BV by proving the normal forms of the structures that are provable in BV. The resulting systems provide a better performance in automated proof search by disabling redundant applications of inference rules due to the unit. As evidence, we provide a comparison of the performance of these systems in a Maude implementation
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: | System BV without the Equalities for Unit |
| Autori: | Kahramanogullari, Ozan |
| Autori Unitn: | |
| Titolo del volume contenente il saggio: | Computer and Information Sciences - ISCIS 2004, 19th International Symposium |
| Luogo di edizione: | Berlin |
| Casa editrice: | Springer-Verlag |
| Anno di pubblicazione: | 2004 |
| Codice identificativo Scopus: | 2-s2.0-35048840154 |
| Codice identificativo ISI: | WOS:000225096700099 |
| ISBN: | 3540235264 |
| Handle: | http://hdl.handle.net/11572/99938 |
| Appare nelle tipologie: | 04.1 Saggio in atti di convegno (Paper in proceedings) |
File in questo prodotto:
http://hdl.handle.net/11572/99938
Copyright © 2021