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

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.

Programs

• The lolliCoP program code in LLP.
• The lolliCoP2 program code in LLP.
• LLP compiler system llp050.tar.gz (including lolliCoP programs in tools directory). Perhaps, you need to compile it with larger memory size setting by modifying the header file "emulator/llpam.h".
• You can use the leanCoP format file to convert TPTP problems for lolliCoP.

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).

• lolliCoP
  • Overall performance (including a list of solved problems rated higher than 0)
  • Detailed result (Problem name, rating, status, first-order/propositional, CPU time in milliseconds)
• lolliCoP2
  • Overall performance (including a list of solved problems rated higher than 0)
  • Detailed result (Problem name, rating, status, first-order/propositional, CPU time in milliseconds)