# EPICC README

## What is it?

Equality Preprocessing In Connection Calculi

## How can I try it out?

Make sure you have the following installed
Java
Python - 3.5 or later
Prolog - SWI-Prolog (http://www.swi-prolog.org/)

Setting up Prolog and the TPTP library path

If you have a problem that requies reading a .ax (TPTP style) file then
the transformation needs to know about the path of the TPTP library.
This can be set using an environmental variable or using a command line
flag. The same is true with your SWI-Prolog path.

Note in both examples the -q flag is used to show a single line of the
proof result. The --timeout flag limits the run time of the final leanCoP
proof procedure to 10 seconds.

Using environment variables:

export PROLOG_PATH=<prolog path>
export TPTP=<tptp path>
./leancop-epicc file -q --timeout 10

Using flags:

./leancop-epicc <file> --prolog <prolog path> --tptp <tptp path> -q --timeout 10

## How does it work?

1. The Problem is read in by the leanCoP transformation module.
2. The (transformed) problem is exported to `<out dir>/<problem name>.trans`
3. EPICC is run on this file and generates a new file `<out dir>/<problem-name>.epicc`
4. The core leanCoP prover is run this '.epicc' file.

### Minimal Example.

Notes:
1. assumes that <out dir> is the directory that leancop-epicc is located in.
2. By default '--epicc-reduction' is set to "red" which is "EPICC-2" (the most performant reduction technique)

./leancop-epicc ~/Documents/TPTP-v6.4.0/Problems/SWC/SWC035+1.p --prolog /usr/local/bin/swipl --tptp ~/Documents/TPTP-v6.4.0 -q

"mm"     = modification method
"axioms" = axioms
"red-lr" = EPICC-1
"red"    = EPICC-2

## Setting custom values

If you want to set custom directories the easiest thing is to run

'leancop-epicc -h'

which gives an explanation of options.

### Example.

./leancop-epicc ~/Downloads/TPTP-v6.4.0/Problems/SWC/SWC036+1.p \
  --prolog /usr/local/bin/swipl                                 \
  --tptp ~/Downloads/TPTP-v6.4.0                                \
  -q                                                            \
  --out-dir ~/Documents/myFolder                                \
  --save-proof-dir ~/Documents/myFolder                         \
  --epicc-reduction red                                         \
  --timeout 10                                                  \

## Clojure source code

The Clojure source code of EPICC is available at

https://github.com/beoliver/clj-epicc/