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 |
