• Automated theorem prover for first-order logic with equality and theories.
• Logic toolkit (logtk), designed primarily for first-order automated reasoning. It aims at providing basic types and algorithms (terms, unification, orderings, indexing, etc.) that can be factored out of several applications.

Zipperposition is intended to be a superposition prover for full first order logic, plus some extensions (datatypes, recursive functions, lambda-free higher order). The accent is on flexibility, modularity and simplicity rather than performance, to allow quick experimenting on automated theorem proving. It generates TSTP traces or graphviz files for nice graphical display.

Zipperposition supports several input formats:

• TPTP (fof, cnf, tff)
• TIP
• its own native input, extension .zf (see directory examples/ and section below)

Zipperposition is written in the functional and imperative language OCaml. The name is a bad play on the words "zipper" (a functional data structure) and "superposition" (the calculus used by the prover), although the current implementation is written in quite an imperative style. Superposition-based theorem proving is an active field of research, so there is a lot of literature about it; for this implementation the main references for the base calculus are:

• the chapter Paramodulation-based theorem proving of the Handbook of Automated Reasoning,
• the paper E: a brainiac theorem prover that describes the E prover by S. Schulz,
• the paper Superposition with equivalence reasoning and delayed clause normal form transformation by H. Ganzinger and J. Stuber

Disclaimer: Note that the prover is a research project. Please don't use it to drive your personal nuclear power plant, nor as a trusted tool for critical applications.

This project is licensed under the BSD2 license. See the LICENSE file.

Zipperposition requires OCaml >= 4.08.0, and some libraries that are available on opam.

The recommended way to install Zipperposition is through opam. You need to have GMP (with headers) installed (it's not handled by opam). Once you have installed GMP and opam, type:

$ opam install zipperposition

To upgrade to more recent versions:

$ opam update
$ opam upgrade

If you want to try the development (unstable) version, which has more dependencies (in particular dune for the build), try:

$ opam pin -k git https://github.com/sneeuwballen/zipperposition.git#master

NOTE: do not install logtk. It now ships with zipperposition itself. NOTE: if installation fails, you might want to try to opam update and opam upgrade: it might be because some of the dependencies are too old.

If you really need to, you can download a release on the following github page for releases.

Look in the file opam to see which dependencies you need to install. They include menhir, zarith, containers, msat and sequence, but maybe also other libraries. Consider using opam directly if possible.

$ make install

Additional sub-libraries can be built if their respective dependencies are met.

If menhir is installed, the parsers library Logtk_parsers will automatically be built.

If you have installed qcheck and alcotest, for instance via opam install qcheck alcotest, you can enable the property-based testing and random term generators with

$ make test

NOTE: in case of build errors, it might be because of outdated dependencies (see via opam for more details), or stale build files. Try rm _build -rf to try to build from scratch.

See this page.

There are some examples of how to use the libraries in src/tools/ and src/demo/.

Typical usage:

$ ./zipperposition.exe examples/ho/SYO265\^5.p --mode ho-competitive --timeout 30
$ ./zipperposition.exe examples/ho/SYO265\^5.p --mode best --timeout 30

Help is available with the option --help. We recommend to set --mode because the default configuration is not great otherwise. For optimal results, use the portfolios (see below).

To build the library, documentation, and tools, type in a terminal located in the root directory of the project:

$ make

If you use ocamlfind (which is strongly recommended), installation/uninstallation are just:

$ make install
$ make uninstall

Zipperposition gives best results when run in a portfolio of different configurations. There is currently no built-in portfolio mode, but we provide python scripts in the directory portfolio to run Zipperposition as a portfolio prover.

To use the portfolio scripts, place a zipperposition binary named zipperposition and a E prover 2.6 binary (with support for higher-order logic) named eprover-ho into the portfolio directory.

There are three different portfolios:

• portfolio.fo.parallel.py: A portfolio optimized for first-order TPTP problems, running on multiple CPUs. The first argument specifies the problem file. The second argument is the timeout. The third argument determines whether all CPUs (true) or all but one CPU (false) are used. Any further arguments are passed on to Zipperposition. Example:

./portfolio.fo.parallel.py ../examples/pelletier_problems/pb10.p 30 true

• portfolio.lams.parallel.py: A portfolio optimized for higher-order TPTP problems, running on multiple CPUs. The first argument specifies the problem file. The second argument is the timeout. The third argument specifies a directory to place temporary files. The forth argument determines whether all CPUs (true) or all but one CPU (false) are used. Any further arguments are passed on to Zipperposition. Example:

./portfolio.lams.parallel.py ../examples/ho/PUZ081^1.p 30 /tmp true

• portfolio.sh.sequential.py: A portfolio optimized for higher-order problems stemming from proof assistants, running on a single CPU. The first argument specifies the problem file. The second argument is the timeout. The third argument specifies a directory to place temporary files. Any further arguments are passed on to Zipperposition. Example:

 ./portfolio.sh.sequential.py ../examples/ho/PUZ081^2.p 30 /tmp

The native syntax, with file extension .zf, resembles a simple fragment of ML with explicit polymorphism. Many examples in examples/ are written using this syntax. A vim syntax coloring file can be found in utils/vim (see the readme for instructions on how to install it).

val i : type.
val a : i.

val f : i -> i. # a function
val p : i -> i -> prop. # a binary predicate

assert forall x y. p x y => p y x.
assert p a (f a).

goal exists (x:i). p (f x) x.

$ ./zipperposition.native example.zf

% done 3 iterations
% SZS status Theorem for 'example.zf'
% SZS output start Refutation
* ⊥/7 by simp simplify with [⊥]/5
* [⊥]/5 by
  inf s_sup- with {X2[1] → a[0]}
    with [p (f a) a]/4, forall (X2:i). [¬p (f X2) X2]/2

* forall (X2:i). [¬p (f X2) X2]/2 by
  esa cnf with ¬ (∃ x/13:i. (p (f x/13) x/13))

* [p (f a) a]/4 by simp simplify with [p (f a) a ∨ ⊥]/3
* [p (f a) a ∨ ⊥]/3 by
  inf s_sup- with {X0[0] → f a[1], X1[0] → a[1]}
    with [p a (f a)]/1, forall (X0:i) (X1:i). [p X0 X1 ∨ ¬p X1 X0]/0

* ¬ (∃ x/13:i. (p (f x/13) x/13)) by
  esa neg_goal negate goal to find a refutation
    with ∃ x/13:i. (p (f x/13) x/13)

* ∃ x/13:i. (p (f x/13) x/13) by goal 'example.zf'
* forall (X0:i) (X1:i). [p X0 X1 ∨ ¬p X1 X0]/0 by
  esa cnf with ∀ x/9:i y/11:i. ((p x/9 y/11) ⇒ (p y/11 x/9))

* [p a (f a)]/1 by esa cnf with p a (f a)
* p a (f a) by 'example.zf'
* ∀ x/9:i y/11:i. ((p x/9 y/11) ⇒ (p y/11 x/9)) by 'example.zf'

% SZS output end Refutation

include "foo.zf".

data nat := Zero | Succ nat.

data list a := nil | cons a (list a).

def four : nat := Succ (Succ (Succ (Succ Zero))).

val set : type -> type.

val member : pi a. a -> set a -> prop.

val union : pi a. set a -> set a -> set a.

rewrite forall a (x:a)(s1:set a)(s2:set a).
  member x (union s1 s2) <=> (member x s1 || member x s2).

val subset : pi a. set a -> set a -> prop.

rewrite forall a (s1:set a)(s2:set a).
  subset s1 s2 <=> (forall x. member x s1 => member x s2).

val equal_set : pi a. set a -> set a -> prop.

rewrite forall a (s1:set a) s2.
  equal_set s1 s2 <=> subset s1 s2 && subset s2 s1.

# now show that union is associative:
goal forall a (s1:set a) s2 s3.
  equal_set
   (union s1 (union s2 s3))
   (union (union s1 s2) s3).

def plus : nat -> nat -> nat where
  forall y. plus Zero y = y;
  forall x y. plus (Succ x) y = Succ (plus x y).

def even : nat -> prop where
  even Zero;
  forall x. even (Succ x) = odd x
and odd : nat -> prop where
  forall x. odd (Succ x) = even x.

$ cat doc/plus_assoc.zf
data nat := Zero | Succ nat.
def plus : nat -> nat -> nat where
  forall y. plus Zero y = y;
  forall x y. plus (Succ x) y = Succ (plus x y).
goal forall (x:nat) y z. plus x (plus y z) = plus (plus x y) z.

$ zipperposition doc/plus_assoc.zf -o none
% done 17 iterations
% SZS status Theorem for 'doc/plus_assoc.zf'

val[AC] f : foo -> foo -> foo.

assert[name "foo"] bar.

A handy way of displaying the proof is to use graphviz:

$ ./zipperposition.native --dot /tmp/example.dot example.zf
$ dot -Txlib /tmp/example.dot

One can generate an image from the .dot file:

$ dot -Tsvg /tmp/example.dot > some_picture.svg

It is possible to avoid displaying the proof at all, by using -o none. A TSTP derivation can be obtained with -o tstp.

Zipperposition's library provides several useful parts for logic-related implementations:

• a library packed in a module Logtk, with terms, formulas, etc.;
• a library packed in a module Logtk_parsers, with parsers for input formats;
• small tools (see directory src/tools/) to illustrate how to use the library and provide basic services (type-checking, reduction to CNF, etc.);

Some advices if you want to hack on the code:

• --debug 5 prints everything the prover does
• --debug.foo <n> changes the verbosity only for foo (see --help for a list of such flags)
• --backtrace is very useful to get stack traces when a wild uncaught exception appears
• --stats prints some statistics, and you can add your own easily with Util.mk_stat
• --dot <some-file>.dot dumps the proof in the given file in graphviz. This is very useful for reading proofs, e.g. using dot -Txlib <some-file>.dot. See Graphical display of proofs for more details.
• many flags control the behavior of the prover; to dumb heuristics down a bit you can try:
  • -cq bfs (BFS traversal of the search space, instead of weight-based clause selection rules)
  • --ord none for disabling term orderings

• a script using perf can be found in utils/profile.sh
• profiling probes are inserted into the code, but they're disabled by default (see src/core/ZProf.ml, let __prof=false). By setting __prof=true the probes will become active, and the command line option --profile will be available.

StarExec is a service for experimental evaluation of logic solvers like Zipperposition.

Name: ssh
Protocol: TCP
Host Port: 3022
Guest Port: 22

starclone login: root
Password: St@rexec

$ yum install openssh-server

$ ssh -p 3022 root@127.0.0.1
root@127.0.0.1's password: St@rexec

$ wget https://raw.github.com/ocaml/opam/master/shell/opam_installer.sh -O - | sh -s /usr/local/bin

$ useradd -m bob
$ passwd bob
New password: bob
BAD PASSWORD: The password is a palindrome
Retype new password: bob
passwd: all authentication tokens updated successfully.

$ exit
$ ssh -p 3022 bob@127.0.0.1
bob@127.0.0.1's password: bob

$ opam init
$ opam switch create 4.12.2
$ eval `opam config env`

$ git clone https://github.com/sneeuwballen/zipperposition.git --branch dev
$ cd zipperposition
$ opam install . --deps-only
$ make

$ exit
$ scp -P 3022 bob@127.0.0.1:~/zipperposition/zipperposition.native  /some/path/on/the/host/machine
bob@127.0.0.1's password: bob

#!/bin/sh

./zipperposition.exe -o tptp "$1" \
  --timeout "$STAREXEC_WALLCLOCK_LIMIT" \
  --mem-limit "$STAREXEC_MAX_MEM"

(experimental)

to build an image:

• docker build -t zipper .

to use the image:

• docker run -i zipper < examples/pelletier_problems/pb47.zf