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

To: Mehdi Dogguy <Mehdi.Dogguy@pps.jussieu.fr>
Cc: 468557@bugs.debian.org
Subject: Bug#468557: ITP: ergo -- Automatic theorem prover dedicated to program verification
From: Florian Weimer <fw@deneb.enyo.de>
Date: Fri, 29 Feb 2008 21:22:45 +0100
Message-id: <[🔎] 87ejavqzqi.fsf@mid.deneb.enyo.de>
Reply-to: Florian Weimer <fw@deneb.enyo.de>, 468557@bugs.debian.org
In-reply-to: <[🔎] 20080229135646.16029.16610.reportbug@potassium.pps.jussieu.fr> (Mehdi Dogguy's message of "Fri, 29 Feb 2008 14:56:46 +0100")
References: <[🔎] 20080229135646.16029.16610.reportbug@potassium.pps.jussieu.fr>

* 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.

Reply to:

Follow-Ups:
- Bug#468557: ITP: ergo -- Automatic theorem prover dedicated to program verification
  - From: Mehdi Dogguy <Mehdi.Dogguy@pps.jussieu.fr>

References:
- Bug#468557: ITP: ergo -- Automatic theorem prover dedicated to program verification
  - From: Mehdi Dogguy <Mehdi.Dogguy@pps.jussieu.fr>

Prev by Date: Bug#467097: ITP: eficas -- ASter Command FIle Editor
Next by Date: Bug#468557: ITP: ergo -- Automatic theorem prover dedicated to program verification
Previous by thread: Bug#468557: ITP: ergo -- Automatic theorem prover dedicated to program verification
Next by thread: Bug#468557: ITP: ergo -- Automatic theorem prover dedicated to program verification
Index(es):
- Date
- Thread