Information for RPM alt-ergo-1.30-15.fc29.src.rpm
| ID | 256738 | ||||||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| Name | alt-ergo | ||||||||||||||||
| Version | 1.30 | ||||||||||||||||
| Release | 15.fc29 | ||||||||||||||||
| 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-08-26 15:49:00 GMT | ||||||||||||||||
| Size | 409.71 KB | ||||||||||||||||
| f5c313a6337d944138da74e8a68f0ef4 | |||||||||||||||||
| License | CeCILL-C | ||||||||||||||||
| Buildroot | f29-build-28019-14838 | ||||||||||||||||
| 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 | ||||||||||||||||
