genz - A Generic Sequent Calculus Prover using the Zipper

Covering the following logics:

• Propositional: CPL, IPL
• Modal: K, K4, K45, T, D, D4, D45, S4, GL

Web interface

You can use the prover online at https://tools.malv.in/genz-web/.

Formula Syntax

Both ASCII and Unicode symbols are allowed. Here are some example formulas:

• [](p -> []p) -> []p
• []p & []q <-> []p | []q which unfolds to ((☐p ∧ ☐q) → (☐p v ☐q)) ∧ ((☐p v ☐q) → (☐p ∧ ☐q)).
• <><>p -> <>p which unfolds to (☐((☐(p → ⊥) → ⊥) → ⊥) → ⊥) → (☐(p → ⊥) → ⊥)

Symbols	Meaning	Note
p, q, bla, ...	atomic propositions
true, ⊤	top (constant true)
false, ⊥	bottom (constant false)
!, ~, ¬	negation (not)	abreviation for ... -> false
&	conjunction (and)	primitive
|, v	disjunction (or)	primitive
->, -->, =>, →,	implication (if-then)	primitive
<->, <-->, <=>,↔	bi-implication (iff)	abbreviation using -> and &.
<>, <a>, ◇	diamond (possible)	abbreviation for ~ [] ~ ...
[], [a], ☐, ◻	box (necessary)	primitive

Building

You should have the Haskell build tool stack installed, via ghcup. For proof visualization, optonally you may want to install graphviz.

To build the project run stack build.

CLI program

To install the genz and the genz-web binaries, just run stack install in this repository.

CLI examples

We can prove a formula given directly with -F or from a file with -f or from standard input with --stdin. By default the modal logic K is used.

$ genz -F "[]p -> [][]p"
False

$ echo "p | ~p" > example.txt
$ genz -f example.txt
True
$ genz -f example.txt --logic IPL
False

$ echo "[][]p -> [][][][]p" | genz --stdin --logic S4
True

Get help:

$ genz --help
genz - a generic sequent calculus prover with zippers

Usage: genz ((-F|--formula FORMULA) | (-f|--file FILE) | (-s|--stdin))
            [-i|--input INPUT] [-t|--tree] [-n|--negate] [-d|--debug]
            [-p|--proofFormat FORMAT] [-l|--logic LOGIC]

  Prove the given FORMULA or the formula in FILE or STDIN.

Available options:
  -F,--formula FORMULA     Formula
  -f,--file FILE           Input file
  -s,--stdin               Read from stdin
  -i,--input INPUT         Input format: single, tptp (default: single)
  -t,--tree                Use standard trees (default is to use zippers).
  -n,--negate              Negate the input formula.
  -d,--debug               Print additional debug information.
  -p,--proofFormat FORMAT  Proof format: none, plain, buss, size (default: none)
  -l,--logic LOGIC         Logic to use: CPL, IPL, D, D4, D45, GL, K, K4, K45,
                           S4, T (default: K)
  -h,--help                Show this help text

Benchmarking zipper vs tree representation (for an unprovable formula):

$ /usr/bin/time -f%E genz -F "[]([]p->p) -> [][][][][][][][][][][][][][][][][][]p" --logic K4
False
0:00.01
$ /usr/bin/time -f%E genz -F "[]([]p->p) -> [][][][][][][][][][][][][][][][][][]p" --logic K4 --tree
False
0:03.44

Haskell examples

You can use stack ghci to run examples like this:

stack ghci lib/Logic/Modal/K.hs lib/FormM.hs

ghci> FormM.multiVerK 3
(☐(3 → (4 → (5 → 1))) → (☐3 → (☐4 → (☐5 → ☐1))))
ghci> FormM.extraAtK 3
(☐(3 → (4 → (5 → (2 → 1)))) → (☐3 → (☐4 → (☐5 → ☐1))))

ghci> isProvableT k (FormM.multiVerK 3)
True
ghci> isProvableZ k (FormM.multiVerK 3)
True
ghci> isProvableT k (FormM.extraAtK 3)
False
ghci> isProvableZ k (FormM.extraAtK 3)
False

In the above k is Logic.Modal.K.k :: Logic, i.e. the proof system.

Defining Your Own Logic

A Logic in GenZ is a collection of safeRules (invertible, applied greedily) and unsafeRules (non-invertible, requiring backtracking and possibly loopchecks):

data Logic f = Log { name :: String
                   , safeRules :: [Rule f]
                   , unsafeRules :: [Rule f] }

Each rule takes a history, the current sequent, and a principal formula, and returns possibly multiple branches:

type Rule f = History f -> Sequent f -> Either f f -> [(RuleName, [Sequent f])]

As an example, CPL has only safe rules:

classical :: Logic FormP
classical = Log { name = "CPL"
                , safeRules   = [leftBot, isAxiom, replaceRule safeCPL]
                , unsafeRules = []
                }

safeCPL :: Either FormP FormP -> [(RuleName,[Sequent FormP])]
safeCPL (Left (ConP f g))   = [("∧L", [Set.fromList [Left g, Left f]])]
safeCPL (Left (DisP f g))   = [("vL", map Set.singleton [Left f, Left g])]
safeCPL (Left (ImpP f g))   = [("→L", map Set.singleton [Right f, Left g])]
safeCPL (Right (ConP f g))  = [("∧R", map Set.singleton [Right f, Right g])]
safeCPL (Right (DisP f g))  = [("vR", [Set.fromList [Right g, Right f]])]
safeCPL (Right (ImpP f g))  = [("→R", [Set.fromList [Right g, Left f]])]
safeCPL _                   = []

For logics that require backtracking (e.g. IPL, modal logics), place non-invertible rules in unsafeRules. See lib/Logic/ for all implemented calculi. Implementation for loopchecks can be found in lib/Logic/Propositional/IPL.hs for reference.

To try your own logic, create a new module under lib/Logic/, following the structure above. Then load it in ghci. Below is an example of a modal logic. You can also define your own language and your own formula examples.

$ stack ghci lib/General.hs lib/FormM.hs lib/Logic/YourLogic.hs
ghci> isProvableZ yourLogic (ImpM (AtM '1') (AtM '1'))
True

LaTeX output

The prover can generate code for bussproofs.

For example

stack exec genz -- -F "□(□p → p) → □p" -l GL -p buss

will print the LaTeX code for the following proof:

When using ghci instead of the genz executable, the following command can be used to write the code into temp.tex and then run pdflatex on it directly:

stack ghci lib/Logic/Modal/GL.hs lib/FormM.hs

ghci> texFile . head . proveZ gl $ ImpM (Box (ImpM (Box (AtM "p")) (AtM "p"))) (Box (AtM "p"))

The Zipper Data Structure

GenZ uses the zipper, a data structure introduced by Huet (1997), to efficiently navigate and modify proof trees during proof search. The idea is to split a tree into a focus (the subtree being worked on) and a path (everything above and around it), enabling constant-time navigation and modification without reconstructing the entire tree.

A standard tree and its zipper in Haskell:

data Tree a    = Node a [Tree a]
data ZipTree a = ZT (Tree a) (Path a)
data Path a    = Top | Step a (Path a) [Tree a] [Tree a]

A ZipTree focuses on a subtree, while Path records the parent node, the path further up, and the left/right siblings. For example, in this tree with focus at node 2:

      0
    / | \ \
   1 [2] 3  4
     |      / \
     5     6   7

ZT (Node 2 [Node 5 []])
   (Step 0 Top [Node 1 []] [Node 3 [], Node 4 [Node 6 [], Node 7 []]])

GenZ applies this to proof search trees via ZipProof and ZipPath:

data ZipProof f = ZP (Proof f) (ZipPath f)
data ZipPath  f = Top | Step (Sequent f) RuleName (ZipPath f) [Proof f] [Proof f]

This makes backtracking efficient: when a rule application fails, GenZ moves the focus back up and tries a different rule without rebuilding the tree.

Tests

To run all tests locally, run stack test. This should not take more than five minutes.

The tests are also run automatically for each commit, see https://github.com/XiaoshuangYang999/GenZ/actions for results.

LWB and ILTP Benchmarks

See the benchmarks folder for bash scripts to run GenZ on these benchmarks.

Custom Benchmarks (bench folder)

You should have LaTeX and pandoc installed.

To run the benchmarks for a small selection of formulas, run make bench/runtime.pdf and make bench/memory.pdf. The runtime benchmark will take around 30 minutes, the memory benchmark less than one minute.

To run benchmarks on a larger set of formulas, run make bench/runtime-all.pdf and make bench/memory-all.pdf. Note: this runtime benchmark will take multiple hours.

Example results are available at https://github.com/XiaoshuangYang999/GenZ/releases.

References

The code in this repository was originally developed as part of the following master's thesis:

• Xiaoshuang Yang: Sequent Calculus with Zippers. University of Amsterdam, 2024. https://eprints.illc.uva.nl/id/eprint/2354

The original code from the thesis can be found in the thesis-version branch. Ongoing updates and improvements are included in the main branch.