Information for RPM alt-ergo-1.30-15.fc30.src.rpm
ID | 316214 | ||||||||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Name | alt-ergo | ||||||||||||||||
Version | 1.30 | ||||||||||||||||
Release | 15.fc30 | ||||||||||||||||
Epoch | |||||||||||||||||
Arch | src | ||||||||||||||||
Summary | Automated theorem prover including linear arithmetic | ||||||||||||||||
Description | Alt-Ergo is an automated theorem prover implemented in OCaml. It is based on CC(X) - a congruence closure algorithm parameterized by an equational theory X. This algorithm is reminiscent of the Shostak algorithm. Currently CC(X) is instantiated by the theory of linear arithmetics. Alt-Ergo also contains a home made SAT-solver and an instantiation mechanism by which it fully supports quantifiers. | ||||||||||||||||
Build Time | 2018-12-09 16:20:25 GMT | ||||||||||||||||
Size | 409.58 KB | ||||||||||||||||
a1e306485f3e4738baee9c3e55ca0d59 | |||||||||||||||||
License | CeCILL-C | ||||||||||||||||
Buildroot | f30-build-41082-22941 | ||||||||||||||||
Provides | No Provides | ||||||||||||||||
Obsoletes | No Obsoletes | ||||||||||||||||
Conflicts | No Conflicts | ||||||||||||||||
Requires |
|
||||||||||||||||
Recommends | No Recommends | ||||||||||||||||
Suggests | No Suggests | ||||||||||||||||
Supplements | No Supplements | ||||||||||||||||
Enhances | No Enhances | ||||||||||||||||
Files |
|
||||||||||||||||
Component of | No Buildroots |