rpms/alt-ergo
3
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
The alt-ergo rpms
112 commits 38 branches 24 tags 292 KiB
Find a file
Exact
Jerry James 11723f084c Version 2.3.3. 
- Add -menhir patch to fix FTBFS.
- Add -stdlib-shims patch since Fedora does not need stdlib-shims.
2022-06-21 09:17:10 -06:00
.gitignore Update to version 2.0.0. 2019-06-05 19:55:51 -06:00
alt-ergo-menhir.patch Version 2.3.3. 2022-06-21 09:17:10 -06:00
alt-ergo-pervasives.patch Version 2.3.3. 2022-06-21 09:17:10 -06:00
alt-ergo-psmt2-frontend.patch Switch to the correct tarball. 2022-02-28 12:02:56 -07:00
alt-ergo-stdlib-shims.patch Version 2.3.3. 2022-06-21 09:17:10 -06: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 Version 2.3.3. 2022-06-21 09:17:10 -06:00
README.md Version 2.3.0. 2021-12-30 17:12:44 -07:00
sources Version 2.3.3. 2022-06-21 09:17:10 -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.