Obsessional cliques: a semantic characterization of bounded time complexity

Authors :: Olivier Laurent
L.T. de Falco
Preuves, Programmes et Systèmes (PPS)
Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS)
Dipartimento di Filosofia
Università degli Studi Roma Tre
Supported by the project ``Coop. Italia/France CNR-CNRS n°19188'. Supported by the French project ``ANR JC05_43380 No-Cost'. Supported by the Italian project ``FOLLIA'
Rajeev Alur
Laurent, O
TORTORA DE FALCO, Lorenzo
Source :: Logic in Computer Science, LICS
Publication Year :: 2006
Publisher :: HAL CCSD, 2006.
Abstract: We give a semantic characterization of bounded complexity proofs. We introduce the notion of obsessional clique in the relational model of linear logic and show that restricting the morphisms of the category RscrEscrLscr to obsessional cliques yields models of ELL and SLL. Conversely, we prove that these models are relatively complete: an LL proof whose interpretation is an obsessional clique is always an ELL/SLL proof. These results are achieved by introducing a system of ELL/SLL untyped proof-nets, which is both correct and complete with respect to elementary/polynomial time complexity

Tools