Information for RPM alt-ergo-1.30-15.fc29.riscv64.rpm
ID | 256742 | |||||||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Name | alt-ergo | |||||||||||||||
Version | 1.30 | |||||||||||||||
Release | 15.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-08-26 15:57:36 GMT | |||||||||||||||
Size | 1.58 MB | |||||||||||||||
e1c9d53b4647f19db4daf44c93809ecd | ||||||||||||||||
License | CeCILL-C | |||||||||||||||
Buildroot | f29-build-28019-14838 | |||||||||||||||
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 |