Zipperposition

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

Short summary

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.

License

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

Build

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

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

Manually

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.

Documentation

See this page.

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

Use

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

Portfolio

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

Native Syntax

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

<details> <summary>Description of the native format `.zf` </summary>

Basics

Comments start with # and continue to the end of the line. Every symbol must be declared, using the builtin type prop for propositions. A type is declared like this: val i : type. and a parametrized type: val array: type -> type.

val i : type.
val a : i.

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

Then, axioms and the goal:

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

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

We can run the prover on a file containing these declarations. It will display a proof very quickly:

$ ./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

Each * -prefixed item in the list is an inference step. The top step is the empty clause: zipperposition works by negating the goal before looking for proving false. Indeed, proving a ⇒ b is equivalent to deducing false from a ∧ ¬b.

Connectives and Quantifiers

The connectives are:

• true: true
• false: false
• conjunction: a && b
• disjunction: a || b
• negation: ~ a
• equality: a = b
• disequality: a != b (synonym for ~ (a = b))
• implication: a => b
• equivalence: a <=> b

Implication and equivalence have the same priority as disjunction. Conjunction binds tighter, meaning that a && b || c is actually parsed as (a && b) || c. Negation is even stronger: ~ a && b means (~ a) && b.

Binders extend as far as possible to their right, and are typed, although the type constraint can be omitted if it can be inferred:

• universal quantification: forall x. F or in its typed form: forall (x:ty). F
• existential quantification: exists x. F

Polymorphic symbols can be declare using pi <var>. type, for instance val f : pi a b. a -> array a b -> b is a polymorphic function that takes 2 type arguments, then 2 term arguments. An application of f will look like f nat (list bool) (Succ Z) empty. Type argume