Bug#468557: ITP: ergo -- Automatic theorem prover dedicated to program verification

[Mehdi Dogguy <Mehdi.Dogguy@pps.jussieu.fr>]

On  0, Florian Weimer <fw@deneb.enyo.de> wrote:
> * Mehdi Dogguy:
> 
> >   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. Ergo contains also a home
> >   made SAT-solver and an instanciation mechanism.
> 
> I think it's "to instantiate" and "instantiation".  The variants with
> "c" aren't that common, and the OED (2nd edition) doesn't list them
> AFAICT.
> 

You're right. I'll fix the description when the package will be uploaded.

-- 
Mehdi Dogguy
http://www.pps.jussieu.fr/~dogguy/