BSD Portsmath/alt-ergo 2.5.4_2 DragonFly
Automatic solver of mathematical formulas for program verification
- System
- DragonFly
- Repository
- DPorts
- Maintainer
- [email protected] (as in FreeBSD)
- License
- CeCILL-C
- Categories
- math
- Package size
- 14247.2 KiB, 65045.4 KiB installed
Description
Alt-Ergo is an automatic theorem prover dedicated to program verification. Alt-Ergo is based on CC(X), a congruence closure algorithm parameterized by an equational theory X. Currently, CC(X) can be instantiated by the empty equational theory and by the linear arithmetics. Alt-Ergo contains also a home made SAT-solver and an instantiation mechanism.
Alt-Ergo is compact, safe, and modular. Each component is described by a small set of inference rules and is implemented as an Ocaml functor.
In the other systems
| System | Port | Version |
|---|---|---|
| DragonFly | math/alt-ergo | 2.5.4_2 |
| FreeBSD | math/alt-ergo | 2.5.4_2 |
| NetBSD | wip/alt-ergo | 1.01 |
| GhostBSD | math/alt-ergo | 2.5.4_2 |
Install
Binary package:
pkg install alt-ergoFrom DPorts:
cd /usr/dports/math/alt-ergo && make install cleanDependencies
Run dependencies 9
No port depends on this one.