-
Notifications
You must be signed in to change notification settings - Fork 1
System Zipperposition
TODO
Zipperposition is a higher-order theorem prover implementing superposition-like calculi (including higher-order ones like lambda superposition and combinatory superposition). The prover was conceived as a testbed for rapidly experimenting with extensions of first-order superposition. Over time it has assimilated many of techniques and heuristics of state-of-the-art first-order superposition prover E and became quite powerful. Still, its first-order performance is a far cry from E’s. Zipperposition is written in OCaml, and features a modular system for adding new rules and techniques to implemented calculi. This makes it attractive for fast evaluation of various promising extensions of superposition.
Zipperposition's source code and licensing information is available at the following github repository: https://github.com/sneeuwballen/zipperposition.git
- Proving
- Model finding
Zipperposition supports many input formats. Most notaby, it supports all TPTP formats from CNF to TH1, but without some features such as $let bindings, tuples and arrays. It also reads SMT-LIB 2 format.
Additionally, Zipperposition features its own .zf format. For the use of this format, please consult the example/ directory of Zipperposition's github repository.
How can a user interpret the output of the system easily (top-level perspective)? If you are following a standard (like TPTP SZS or SMT-Lib) just say so. If not, you can provide a table with common outputs (please adjust the following template as you see fit):
| Output | Meaning |
|---|---|
Heureka x! |
The system found a proof for input file x. |
No can do x |
The system did not succeed in establishing any result for input file x. |
Error error |
Something went wrong. |
Zipperposition can output proofs in TSTP and .zf formats.
Remove comments (tags) of unsupported proof formats (and then also remove this line).
https://github.com/sneeuwballen/zipperposition.git
Zipperposition is deployed with the default installation of Isabelle and enabled by default as a backend to Sledgehammer. It is also used as a backend to TLA+ system. It performs well on THF category of CASC theorem prover comptetition: Zipperposition won this division in 2020 and 2021 editions of CASC.
Maintained
If possible, give a list of papers/documents (preferrably via DOIs) that give further details to the system.