[Prev][Next][Index][Thread]

ABSTRACT





A new correctness criterion for proof-structures in MLL

DEFINITION:
In a CPS (concrete proof-structures) we denote by
       n ---> number of terminal formulas
       k ---> number of times-links
       p ---> number of par-links

The following theorem holds:

THEOREM
A CPS is an SPS iff it satisfies the following conditions:
(1) it is a connected graph and if one removes in any way exactly one edge from
each par-link, the connection of the structure is preserved
(2) n=k-p+2.

Giorgia Ricci
Dipartimento di Matematica
Universita' di Siena
Via del Capitano 15
53100 SIENA - Italy -
fax  (577) 263730
e-mail RICCIGIOR@SIVAX.CINECA.IT