Information for RPM alt-ergo-2.3.3-11.fc40.src.rpm
| ID | 1091596 | ||||||||||||||||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| Name | alt-ergo | ||||||||||||||||||||||||||
| Version | 2.3.3 | ||||||||||||||||||||||||||
| Release | 11.fc40 | ||||||||||||||||||||||||||
| 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 | 2023-11-13 09:32:41 GMT | ||||||||||||||||||||||||||
| Size | 2.83 MB | ||||||||||||||||||||||||||
| baa449884f69431a0057c9fbdb9b2160 | |||||||||||||||||||||||||||
| License | Apache-2.0 AND LGPL-2.1-only WITH OCaml-LGPL-linking-exception | ||||||||||||||||||||||||||
| Buildroot | f40-build-739935-109388 | ||||||||||||||||||||||||||
| 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 | ||||||||||||||||||||||||||
