math/eprover 2.6_2 FreeBSD
Theorem prover for full first-order logic with equality
- System
- FreeBSD
- Repository
- FreeBSD ports
- Maintainer
- [email protected]
- License
- LGPL20+, GPLv2+
- Categories
- math
- Package size
- 888.4 KiB, 10880.6 KiB installed
Description
A saturating theorem prover for full first-order logic with equality. It accepts a problem specification, typically consisting of a number of first-order clauses or formulas, and a conjecture, again either in clausal or full first-order form. The system will then try to find a formal proof for the conjecture, assuming the axioms.
In the other systems
| System | Port | Version |
|---|---|---|
| FreeBSD | math/eprover | 2.6_2 |
| DragonFly | math/eprover | 2.6_2 |
Install
Binary package:
pkg install eproverFrom the ports tree:
cd /usr/ports/math/eprover/ && make install cleanTo depend on this port in another port's Makefile:
RUN_DEPENDS= eprover>0:math/eproverPackages
The version each package repository carries. “-” means the repository builds no package of it, “n/a” that there is no such repository.
| Repository | aarch64 | amd64 | armv6 | armv7 | i386 |
|---|---|---|---|---|---|
| FreeBSD:14:latest | 2.6_2 | 2.6_2 | 2.0_1 | 2.6_2 | 2.6_2 |
| FreeBSD:14:quarterly | 2.6_2 | 2.6_2 | n/a | 2.6_2 | 2.6_2 |
| FreeBSD:15:latest | 2.6_2 | 2.6_2 | n/a | 2.6_2 | 2.6_2 |
| FreeBSD:15:quarterly | 2.6_2 | 2.6_2 | n/a | n/a | n/a |
| FreeBSD:16:latest | 2.6_2 | 2.6_2 | n/a | n/a | n/a |
| FreeBSD:16:quarterly | n/a | n/a | n/a | n/a | n/a |
Dependencies
As this port's Makefile names them.
Build 2
bash: shells/bashhelp2man: misc/help2man
Runtime 1
bash: shells/bash
The full lists below include those, and their dependencies in turn.
Build dependencies 7
Run dependencies 3
No port depends on this one.
Configuration
No options to configure.
- USES
- gmake shebangfix
- Service scripts
- none
Files
Manual pages 12
- checkproof(1)
- e_axfilter(1)
- e_deduction_server(1)
- e_ltb_runner(1)
- e_stratpar(1)
- eground(1)
- ekb_create(1)
- ekb_delete(1)
- ekb_ginsert(1)
- ekb_insert(1)
- epclextract(1)
- eprover(1)
pkg-plist 24
- bin/checkproof
- bin/e_axfilter
- bin/e_deduction_server
- bin/e_ltb_runner
- bin/e_stratpar
- bin/eground
- bin/ekb_create
- bin/ekb_delete
- bin/ekb_ginsert
- bin/ekb_insert
- bin/epclextract
- bin/eprover
- share/man/man1/checkproof.1.gz
- share/man/man1/e_axfilter.1.gz
- share/man/man1/e_deduction_server.1.gz
- share/man/man1/e_ltb_runner.1.gz
- share/man/man1/e_stratpar.1.gz
- share/man/man1/eground.1.gz
- share/man/man1/ekb_create.1.gz
- share/man/man1/ekb_delete.1.gz
- share/man/man1/ekb_ginsert.1.gz
- share/man/man1/ekb_insert.1.gz
- share/man/man1/epclextract.1.gz
- share/man/man1/eprover.1.gz
distinfo 1
| File | Size | SHA256 |
|---|---|---|
| eprover-eprover-E-2.6_GH0.tar.gz | 1.709485e+06 | 401ecbe4e9abd1a89df47a74929ea970bbde5e863ad9f9f672b24434fa8259ca |
Commit history 0
No commits in the history this site was built from.