7 lines
412 B
Plaintext
7 lines
412 B
Plaintext
Alt-Ergo is an automatic theorem prover dedicated to program
|
|
verification. Alt-Ergo is based on CC(X) a congruence closure algorithm
|
|
parameterized by an equational theory X. Currently, CC(X) can be instantiated
|
|
by the empty equational theory and by the linear arithmetics. Alt-Ergo
|
|
contains also a home made SAT-solver and an instantiation mechanism. Its
|
|
architecture is summarized by the the following picture.
|