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
References in zbMATH (referenced in 3 articles )
Showing results 1 to 3 of 3.
- Chaudhuri, Kaustuv; Pfenning, Frank; Price, Greg: A logical characterization of forward and backward chaining in the inverse method (2008)
- Otten, Jens; Bibel, Wolfgang: IeanCOP: lean connection-based theorem proving (2003)
- Vana, Leonardo B.; Da S.Corr^ea, Marcelo: A tableau method for the lambek calculus based on a matrix characterization. (2003)