The alt-ergo rpms
Find a file
Fedora Release Engineering 43489678ca Rebuilt for https://fedoraproject.org/wiki/Fedora_37_Mass_Rebuild
Signed-off-by: Fedora Release Engineering <releng@fedoraproject.org>
2022-07-20 20:41:54 +00:00
.gitignore Update to version 2.0.0. 2019-06-05 19:55:51 -06:00
alt-ergo-dune3.patch Patch out uses of the dune external-lib-deps command. 2022-07-05 17:03:29 -06:00
alt-ergo-forward-compat.patch Patch out uses of the dune external-lib-deps command. 2022-07-05 17:03:29 -06:00
alt-ergo-menhir.patch Version 2.3.3. 2022-06-21 09:01:13 -06:00
alt-ergo-pervasives.patch Version 2.3.3. 2022-06-21 09:01:13 -06:00
alt-ergo-psmt2-frontend.patch Switch to the correct tarball. 2022-02-28 12:02:56 -07:00
alt-ergo.desktop Add desktop icons. 2014-03-24 12:59:13 -06:00
alt-ergo.metainfo.xml Updates to the desktop and metainfo files. Add -pervasives patch. 2021-02-04 09:01:16 -07:00
alt-ergo.spec Rebuilt for https://fedoraproject.org/wiki/Fedora_37_Mass_Rebuild 2022-07-20 20:41:54 +00:00
README.md Version 2.3.0. 2021-12-30 17:12:44 -07:00
sources Version 2.3.3. 2022-06-21 09:01:13 -06:00

alt-ergo

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.