[Prev][Next][Index][Thread]
papers available
A number of recent papers related to linear logic
are available by anonymous ftp from
ftp.informatik.uni-tuebingen.de:
1) File /pub/LS/lamlog.{ps,dvi}.Z:
Classical Lambek Logic
by J. Hudelmaier and P. Schroeder-Heister.
A paper about proof theoretical properties of the two sided
version of classical noncommutative linear logic. In particular
we formulate a cut free yet complete sequent calculus for this logic.
2) File /pub/LS/hier.ps.Z:
On a hierarchy of fragments of intuitionistic propositional logic
by J. Hudelmaier.
We give a simple syntactic definition of a hierarchy H of sets of
so called CD-sequents such that intuitionistic provability of
the sequents in the stages of H is hard for successive stages of
the polynomial hierarchy. Moreover provability for the set of all
CD-sequents is PSPACE complete. One corollary says that the CD-
sequents provide a polynomial normal form for intuitionistic
propositional logic. Another corollary is
3) File /pub/LS/comp.ps.Z:
On the complexity of commutative and noncommutative linear logic
by J. Hudelmaier.
Here we show that the fragment of both commutative and noncommutative
linear logic based on (one) implication and additive conjunction
is PSPACE complete.
4) File /pub/LS/modal.ps.Z:
On a contraction free sequent calculus for the modal logic S4
by J. Hudelmaier.
We formulate a sequent calculus for S4 in which deductions of
sequents are bounded in length by the length of the endsequent.
The calculus is much more complicated than similar calculi for
intuitionistic propositional logic. But it may be possible to use
this calculus for an embedding of S4 into linear logic without
modalities in a manner similar to what has been done for
intuitionistic implication.
5) File /pub/LS/KTS4.ps.Z:
Improved decision procedures for the modal logics K,T, and S4
by J. Hudelmaier.
Using methods developped in 4) we arrive at decision procedures of
space complexity n log n, n log n, n*n log n for the logics K,
T, and S4 respectively.
Joerg Hudelmaier