coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: Vladimir Komendantsky <komendantsky AT gmail.com>
To: Razvan Voicu <razvan AT comp.nus.edu.sg>
Cc: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] Pointers to automation of proof by induction
Date: Tue, 28 Apr 2009 10:14:27 +0100
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type:content-transfer-encoding; b=ckaJQSt6e+h4ltB4FgMMcXUAS+qlkMphhJiGj85oon8jpgMPHl6ELWXoIJRIaN8PA7 XcqVTW6U56IY9HinRwpOyhnDyul075K9A3bfpdzBM1MmV2i3ytdWC9/5DCBzyNYBf7mX pDyAy5YeyNmHOGKKk3pFt+xDc+0TGtsbAMT1s=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hi Razvan,

There is our paper with Yves Bertot
http://hal.inria.fr/inria-00190975/en/ about an automated command
written in both Coq and Ocaml and relying on some classical logic
reasoning. Although the command itself is still only partially
implemented. It is available at
http://www-sop.inria.fr/marelle/Vladimir.Komendantsky/ffcpo-20080502.tgz.

I hope this is useful for your references.

Best wishes,
Vladimir

[Coq-Club] Pointers to automation of proof by induction, Razvan Voicu
- Re: [Coq-Club] Pointers to automation of proof by induction, Lucas Dixon
- Re: [Coq-Club] Pointers to automation of proof by induction, Vladimir Komendantsky
- Re: [Coq-Club] Pointers to automation of proof by induction, Pierre Courtieu
  - Re: [Coq-Club] Pointers to automation of proof by induction, Razvan Voicu