linTAP

linTAP is a tableau prover for the multiplicative and exponential fragment of Girards linear logic. It proves the classical validity of a given formula by constructing an analytic tableau and ensures the linear validity using prefix unification. Due to the compact code the program can easily be modified for special purposes or applications. Features of linTAP: Theorem prover for the multiplicative, exponential fragment M?LL of linear logic. Based on a prefixed semantic tableau calculus. Sound and complete. Source code available for popular Prolog systems, including ECLiPSe Prolog, SWI-Prolog and SICStus Prolog. Simple input format.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element