使用 Homebrew, apt, Nix, dnf, MacPorts 安装 eprover

项目链接

• 主页
• 仓库
• 上游文档
• 软件包管理器页面

命令和别名

• checkproof
• e_axfilter
• e_deduction_server
• e_ltb_runner
• e_stratpar
• eground
• ekb_create
• ekb_delete
• ekb_ginsert
• ekb_insert
• epclextract
• eprover
• picosat

项目历史

Development of E started as part of the E-SETHEO project at the Technical University of Munich. The official page says the first public release was in 1998 and that the system has been continuously improved since then.

E grew from a first-order automated theorem prover into a family of command-line tools around proof search, proof checking, axiom filtering, grounding, and related workflows. The 3.x line added full higher-order logic support and improved multicore scheduling, while the current site advertises E 3.2.

采用历史

E has a long competition record. The official awards page says E has participated on its own or as part of E-SETHEO in every CASC competition since 1999, has routinely placed among the top provers in several first-order categories, and has also been used as a subcomponent by other competitors.

Package adoption is helped by E's academic visibility and command-line packaging shape. The project distributes source releases, documents Unix man pages and a PDF manual, and is packaged in Homebrew, Debian, Ubuntu, Nix, and related ecosystems.

使用方式

The official usage page recommends starting with automatic mode, for example eprover --auto problem.p, and using strategy scheduling for multicore runs. Inputs are typically in TPTP/TSTP syntax, and newer versions can produce answer substitutions for existential questions.

E also ships documentation with the distribution, including README files, Unix man pages for major executables, --help output, and the E manual in E/DOC/eprover.pdf.

为什么软件包爱好者会关心

E is significant because it is a serious research prover that still behaves like a Unix toolchain: source tarballs, man pages, many small executables, CLI flags, and benchmark-oriented releases. It is the kind of scientific package where reproducible command lines matter.

时间线

• 1998: First public release of E.
• 1999: E begins its long-running CASC competition participation.
• 2017: E 2.0 adds support for many-sorted logic through TPTP TFF.
• 2023: E 3.0 adds full higher-order logic support and improved multicore scheduling.
• 2024: E 3.1 is released.
• 2026: E 3.2 is listed as the current release on the official site.

Related projects

• E-SETHEO is the project context from which E originated.
• TPTP/TSTP are the problem and proof syntaxes emphasized in E's usage documentation.
• PicoSAT is integrated in parts of the E distribution and appears among packaged executables.

来源

• https://wwwlehre.dhbw-stuttgart.de/~sschulz/E/E.html
• https://wwwlehre.dhbw-stuttgart.de/~sschulz/E/Usage.html
• https://wwwlehre.dhbw-stuttgart.de/~sschulz/E/Awards.html
• https://wwwlehre.dhbw-stuttgart.de/~sschulz/E/Archive.html
• https://github.com/eprover/eprover
• https://api.github.com/repos/eprover/eprover