Linear logic merupakan sebuah logika yang dirancang oleh Jean-Yves Girard sebagai perbaikan dari logika klasik yang sudah ada. Kekuatan dari linear logic terletak pada interpretasi formula sebagai sebuah resource. Tugas Akhir ini mengembangkan sebuah theorem prover untuk linear logic yang diberi nama LinProver. Metode theorem proving yang dilakukan adalah metode tableau. Implementasi dari metode tersebut dilakukan dengan SWI-Prolog. Parsing masukan dilakukan dengan menggunakan definite clause grammar (DCG). Hasil uji coba terhadap implementasi menunjukkan kebenaran dari program. Namun masih dibutuhkan peningkatan kinerja untuk running time.