GenZ-0.1.0.0: README.md
# 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](https://www.haskell.org/ghcup/).
For proof visualization, optonally you may want to install [`graphviz`](https://graphviz.org/).
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):
```haskell
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:
```haskell
type Rule f = History f -> Sequent f -> Either f f -> [(RuleName, [Sequent f])]
```
As an example, CPL has only safe rules:
```haskell
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", [Set.singleton (Left f), Set.singleton (Left g)])]
safeCPL (Left (ImpP f g)) = [("→L", [Set.singleton (Right f), Set.singleton (Left g)])]
safeCPL (Right (ConP f g)) = [("∧R", [Set.singleton (Right f), Set.singleton (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](https://ctan.org/pkg/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)](https://doi.org/10.1017/S0956796897002864), 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:
```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`:
```haskell
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](https://pandoc.org/) 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.