this repo has no description
anil.recoil.org
1opam-version: "2.0"
2homepage: "https://github.com/Deducteam/zenon_modulo"
3dev-repo: "git+https://github.com/Deducteam/zenon_modulo.git"
4maintainer: "Guillaume Burel <guillaume.burel@ensiie.fr>"
5authors: [ "INRIA and contributors" ]
6license: "BSD-3-Clause"
7bug-reports: "https://github.com/Deducteam/zenon_modulo/issues"
8tags: [ "automated theorem prover" ]
9depends: [
10 "ocaml" {>= "4.08.0"}
11 "zarith" {>= "1.11"}
12]
13depopts: [
14 "coq"
15]
16build: [
17 ["./configure"
18 "--prefix" prefix
19 "--libdir" lib]
20 [make]
21]
22install: [[make "install"]]
23conflicts: ["ocaml-option-bytecode-only"]
24synopsis: "Zenon Modulo Theory"
25description: """
26Automated theorem prover for first order classical logic (with
27equality), based on the tableau method. Zenon_modulo handles first-order
28logic with equality. Its most important feature is that it outputs the
29proofs of the theorems, in Coq-checkable form."""
30url {
31 src:
32 "https://github.com/Deducteam/zenon_modulo/archive/refs/tags/0.5.0.tar.gz"
33 checksum: [
34 "md5=3e0a13775df0546b02d8d77d3834d777"
35 "sha512=9b70eddb40404011c4b593604c9974c3f81ffeac119ad190be3aa2964f98c60ee166aeff07eee62d51f26df9663e65eea4e181812ef0077892a421b50f1bc4f6"
36 ]
37}