FREE SOFTWARE ON CAMLCITY.ORG
Automated first-order theorem prover
From the ergo web site: Ergo is an automatic theorem prover dedicated to program verification. Ergo is based on CC(X) a congruence closure algorithm parameterized by an equational theory X. Currently, CC(X) can be instanciated by the empty equational theory and by the linear arithmetics.
| Version: | 0.9.4 |
| Homepage: | http://alt-ergo.lri.fr |
| Maintainer: | Virgile Prevosto <virgile.prevosto@m4x.org> |
| Files: |
bin/alt-ergo lib/alt-ergo/altErgo.cmi lib/alt-ergo/altErgo.cmi_pretty lib/alt-ergo/altErgo.cmo lib/alt-ergo/altErgo.cmx lib/alt-ergo/altErgo.o share/man/man1/alt-ergo.1.html |
| Built from sources: |
alt-ergo-0.94 |