zipperposition
Zipperposition is a superposition prover for full first order logic with equality.
Description
The accent is on flexibility, modularity and simplicity rather than performance, to allow quick experimenting on automated theorem proving. It generates TSTP traces and features many simplification rules and redundancy criteria.
Install
copied = false, 2000)"
:class="{ 'border-gray-700': !copied, 'text-gray-100': !copied, 'focus:ring-orange-500': !copied, 'focus:border-orange-500': !copied, 'border-green-600': copied, 'text-green-600': copied, 'focus:ring-green-500': copied, 'focus:border-green-500': copied }">
- Published
- 29 Jul 2016
- Authors
- Maintainers
Sources
Dependencies
msat
>= "0.3" & < "0.4"
sequence
>= "0.4" & < "0.9"
containers
> "0.16" & < "1.0"
ocamlfind
build
ocaml
>= "4.02.3"
Reverse Dependencies
Conflicts
sequence
>= "0.9"
containers
>= "1.2"