Information for RPM alt-ergo-1.30-15.fc30.riscv64.rpm
ID | 316222 | |||||||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Name | alt-ergo | |||||||||||||||
Version | 1.30 | |||||||||||||||
Release | 15.fc30 | |||||||||||||||
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-12-09 17:46:07 GMT | |||||||||||||||
Size | 1.58 MB | |||||||||||||||
8cb4f51f0e3373605dabb7a8f689eee9 | ||||||||||||||||
License | CeCILL-C | |||||||||||||||
Buildroot | f30-build-41082-22941 | |||||||||||||||
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 |