Title :
The complexity of neutrals in linear logic
Author :
Kanovich, Max I.
Author_Institution :
Dept. of Inf. Eng., Tohoku Univ., Sendai, Japan
Abstract :
The main result announced in the paper is the proof of the existence of strongly independent (free) sets of linear logic formulas that are built up of only neutrals. The motivating application is a uniform and transparent technique for obtaining the exact computational characterization of constant only fragments of commutative and noncommutative linear logic. In particular, we prove the surprising results that: multiplicative additive fragments of constant only linear logic are PSPACE complete; all partial recursive predicates are directly definable in the full constant only linear logic
Keywords :
computational complexity; formal logic; theorem proving; PSPACE complete; constant only fragments; directly definable; exact computational characterization; full constant only linear logic; linear logic formulas; multiplicative additive fragments; neutrals; noncommutative linear logic; partial recursive predicates; proof; strongly independent sets; transparent technique; Boolean functions; Logic; Vectors;
Conference_Titel :
Logic in Computer Science, 1995. LICS '95. Proceedings., Tenth Annual IEEE Symposium on
Conference_Location :
San Diego, CA
Print_ISBN :
0-8186-7050-9
DOI :
10.1109/LICS.1995.523282