rpms/alt-ergo
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
The alt-ergo rpms
149 commits 38 branches 24 tags 292 KiB
Find a file
Exact
Fedora Release Engineering 259c21b750 Rebuilt for https://fedoraproject.org/wiki/Fedora_44_Mass_Rebuild
2026-01-16 03:37:12 +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-inline-error.patch Add patch to fix misplaced inline attributes 2024-05-23 10:57:15 -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 Update metainfo contact address 2023-12-18 20:31:53 -07:00
alt-ergo.spec Rebuilt for https://fedoraproject.org/wiki/Fedora_44_Mass_Rebuild 2026-01-16 03:37:12 +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

README.md

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.