We reduce the provability of fragments of multiplicative linear logic to matching problems consisting in finding a one-one-correspondence between two sets of first-order terms together with a unifier that equates the corresponding terms. According to the kind of structure to which these first-order terms belong our matching problem corresponds to provability in the implicative fragment of multiplicative linear logic, in the Lambek calculus, or in the non-associative Lambek calculus.
CITATION STYLE
de Groote, P. (2000). Proof-search in implicative linear logic as a matching problem. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1955, pp. 257–274). Springer Verlag. https://doi.org/10.1007/3-540-44404-1_17
Mendeley helps you to discover research relevant for your work.