# Intellectics Group: Technical Report 99-04

## linTAP: A Tableau Prover for Linear Logic

### Heiko Mantel and Jens Otten

linTAP is a tableau prover for the multiplicative and
exponential fragment M?LL of Girards linear logic. It
proves the validity of a given formula by constructing
an analytic tableau and ensures the linear validity using
prefix unification. We present the tableau calculus used
by linTAP, an algorithm for prefix unification in linear
logic, the linTAP implementation, and some experimental
results obtained with linTAP.