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 (MLL) with the rules mix, nullary mix, and a self-dual, noncommutative logical operator, called seq. While the rules mix and nullary mix extend the deductive system, the operator seq extends the language of MLL. Due to the operator seq, system BV extends the applications of MLL to those where the sequential composition is crucial, e.g., concurrency theory. System FBV is an extension of MLL with the rules mix and nullary mix. In this paper, by relying on the fact that system BV is a conservative extension of system FBV, I show that system BV is NP-complete by encoding the 3-Partition problem in FBV. I provide a simple completeness proof of this encoding by resorting to a novel proof theoretical method for reducing nondeterminism in proof search, which is also of independent interest.
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 is NP-complete |
| Autori: | Kahramanogullari, Ozan |
| Autori Unitn: | |
| Titolo del periodico: | ANNALS OF PURE AND APPLIED LOGIC |
| Anno di pubblicazione: | 2008 |
| Numero e parte del fascicolo: | 1–3 |
| Codice identificativo Scopus: | 2-s2.0-39549101770 |
| Codice identificativo ISI: | WOS:000254378600007 |
| Digital Object Identifier (DOI): | http://dx.doi.org/10.1016/j.apal.2007.11.005 |
| Handle: | http://hdl.handle.net/11572/99753 |
| Appare nelle tipologie: | 03.1 Articolo su rivista (Journal article) |
File in questo prodotto:
http://hdl.handle.net/11572/99753
Copyright © 2021