Information for RPM alt-ergo-1.30-12.fc29.riscv64.rpm
ID | 153165 | |||||||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Name | alt-ergo | |||||||||||||||
Version | 1.30 | |||||||||||||||
Release | 12.fc29 | |||||||||||||||
Epoch | ||||||||||||||||
Arch | riscv64 | |||||||||||||||
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-06-26 20:17:33 GMT | |||||||||||||||
Size | 1.59 MB | |||||||||||||||
ee53fefe49eff63c677383ee50be602f | ||||||||||||||||
License | CeCILL-C | |||||||||||||||
Buildroot | f29-build-14836-6860 | |||||||||||||||
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 |