Handsome Non-Commutative Proof-Nets: perfect matchings, series-parallel orders and Hamiltonian circuits

Sylvain Pogodalla (1) , Christian Retoré (2)

1 CALLIGRAMME - Linear logic, proof networks and categorial grammars
2 SIGNES - Linguistic signs, grammar and meaning: computational logic for natural language

This paper provides a definition of proof-nets for non-commutative linear logic (cyclic linear logic and Lambek calculus) where there are no links, that are small graphs representing the connectives. Instead of a tree like representation with links, the formula is depicted as a graph representing the conclusion up to the algebraic properties of the connectives. In the commutative case the formula is viewed as a cograph. In the non-commutative case it is a more complicated kind of graph which is, roughly speaking, a directed cograph. The criterion consists in the commutative condition plus a bracketing condition.

Mots clés: proof theory; linear logic; graph theory; perfect matching; cographs; cyclic orders; computational linguistics; lambek calculus; categorial grammars

Domaines: Autre [cs.OH]

Sylvain Pogodalla, Christian Retoré. Handsome Non-Commutative Proof-Nets: perfect matchings, series-parallel orders and Hamiltonian circuits. [Research Report] RR-5409, INRIA. 2004, pp.25. ⟨inria-00071248⟩