lolliCoP: A Linear Logic Implementation of A Lean Connection-Method Theorem Prover

Last modified: Sat Aug 20 01:32:25 2011 JST

lolliCoP is a Lolli/ LLP re-implementation of the lean connection-based theorem prover leanCoP 1.0 developed by Jens Otten.

lolliCoP is a compact theorem prover for first-order classical (clausal) logic written in a linear logic programming language Lolli and executed under LLP compiler.


Performance on the TPTP Problems

The following results are obtained by executing the provers for 2200 problems of TPTP library version 2.3.0 on a Linux machine (Pentium III 550MHz, 128M bytes memory). The time limit for all proof attempts was 300 seconds. The version of LLP compiler is 0.50 (Heap: 1M, Stack: 1M, Trail: 3M, PDL: 100K, Resource table: 20K, Hash table : 10K).

Joshua S. Hodas / Naoyuki Tamura