Basics

Comments start with# and continue to the end of the line. Every symbol must be declared, using the builtin typeprop 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 functionval 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 proveron 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 provingfalse. Indeed, provinga ⇒ b is equivalent to deducingfalse froma ∧ ¬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 thata && 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 usingpi <var>. type, for instanceval f : pi a b. a -> array a b -> b is a polymorphic function that takes 2 type arguments, then 2 term arguments. An application off will look likef nat (list bool) (Succ Z) empty. Type arguments might be omitted if they can be inferred.

Inclusion

It can be convenient to put commonly used axioms in a separate file. The statement

include "foo.zf".

will include the corresponding file (whose path is relative to the current file).

Advanced Syntax

There are more advanced concepts that are mostly related to induction:

• datatypes: (here, Peano numbers and polymorphic lists)

data nat := Zero | Succ nat.data list a := nil | cons a (list a).

• simple definitions:

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

• rewrite rules:

A rewrite rule is similar to anassert statement, except it is much more efficient. Zipperposition assumes that the set of rewrite rules in its input isconfluent andterminating (otherwise, no guarantee applies). Rewriting can be done on terms and on atomic formulas:

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

there are several variations on literal rewrite rules:

• rewrite forall x. p x (short forp x <=> true)

• rewrite forall x. ~ p x (short forp x <=> false)

• rewrite forall x. p x => q x (one way rule, will rewritep x but not~ p x; also calledpolarized rewriting)

• rewrite forall x. ~ p x => q x (negative polarized rule)

• recursive definitions:

one can write recursive functions (assuming they terminate), they will be desugared to a declaration + a set of rewrite rules:

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

Mutually recursive definitions are separated byand:

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

Zipperposition is able to do simple inductive proofs using these recursive functions and datatypes:

$ cat doc/plus_assoc.zfdata 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'

• conditionals:

tests on boolean formulas are writtenif a then b else c, wherea:prop,b, andc, are terms.b andc must have the same type.

• pattern-matching:

shallow pattern matching is writtenmatch <term> with [case]+ end where each case is| <constructor> [var]* -> <term>.

• AC symbols:

Some symbols can be declared "associative commutative": they satisfy

• forall x y z. f x (f y z) = f (f x y) z

• forall x y. f x y = f y x.

the following statement is a bit more efficient than writing the corresponding axioms:

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

• Axioms inSet of Support:

Some axioms (introduced usingassert [sos] <formula>.) will be considered as part of the so-called "set of support" strategy. No saturation among SOS axioms is done. They are only used for inferences (and simplifications) with non-SOS axioms and goals. Typically this is useful for introducing general lemmas while preventing them from interacting in ways not related to the current goal.

• Named Axioms:

An axiom can be given a name, as in TPTP, to retrieve it easily in proofs. The syntax is:

assert[name "foo"] bar.

The easiest way to import Zipperposition as a solver is to pre-compile Zipperposition on theStarExec virtual machine. Download the VM image and open it in VirtualBox.

Open the settings of the VM. Set "Network > Adapter 1 > Attached to" to NAT to have internet access from inside the VM. To allow SSH access into the VM open "Network > Adapter 1 > Advanced > Port Forwarding" and create a new rule:

Name: sshProtocol: TCPHost Port: 3022Guest Port: 22

Leave the two IP fields empty.

Start the VM. Log in as root using the password "St@rexec".

starclone login: rootPassword: St@rexec

Install the openssh server to get a more convenient access to the machine and to copy the compiled binary later.

$ yum install openssh-server

Now open a terminal on the host machine while the VM is still running. Tunnel into the VM via SSH:

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

Install OPAM:

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

So far we have used the superuser root. To download and compile Zipperposition we will use a regular user that we create as follows:

$ useradd -m bob$ passwd bobNew password: bobBAD PASSWORD: The password is a palindromeRetype new password: bobpasswd: all authentication tokens updated successfully.

Close the SSH connection and reopen it as the new user:

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

Initialize OPAM. Install OCaml 4.05 and the dependencies of Zipperposition (Look in the fileopam to see which dependencies you need to install).

$ opam init$ opam switch 4.05.0+flambda$ eval `opam config env`$ opam install dune zarith containers sequence msat menhir

Clone Zipperposition and compile it:

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

Close the SSH connection and copy the binary from the VM onto your host machine.

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

As describedin the StarExec documentation you need a script whose filename has the prefixstarexec_run_ to execute your solver. For Zipperposition this script could look like this:

#!/bin/sh./zipperposition.native -o tptp "$1" \  --timeout "$STAREXEC_WALLCLOCK_LIMIT" \  --mem-limit "$STAREXEC_MAX_MEM"

Put this script and the filezipperposition.native into a folder calledbin. Create a ZIP archive containing that folder. Now Zipperposition is ready to be uploaded to StarExec!

• edit*.opam files to update the version number (fieldversion).

• git commit -a -m "prepare for <version>" (to save the changes on the stable branch)

• make clean all (to check everything builds properly)

• git tag <version> (e.g.git tag 1.4)

• git push origin <version> (origin being the name of the github remote)

• opam publish prepare zipperposition.1.4 https://github.com/sneeuwballen/zipperposition/archive/1.4.tar.gz (using the actual version number). This might require toopam install opam-publish first, it's a handy opam plugin for managing releases.

• if that works properly, then it will create a directoryzipperposition.<version>. Just runopam publish submit zipperposition.1.4 to open a PR against opam-repository.

If something is wrong with the release, it's possible to change it. This is a bit brutal,never do it for older releases that have been merged into opam-repo, only for the next release while no one has seen it yet.

• git tag -f <version>; git push origin :<version> ; git push origin <version> to change the tag

• re-run the twoopam publish commands to update the directory and the PR.