The Coq mailing list

[Lucas Dixon <ldixon AT inf.ed.ac.uk>]

Hi Razvan,

I have a list of inductive theorem proving systems, alive and
sleeping-or-dead, at:

http://dream.inf.ed.ac.uk/projects/isaplanner/wiki/InductiveProversOfTheWorld

I would welcome additions/corrections to this. I am hoping to improve
the list an include some more descriptions of each system as well as
problems that help clarify the distinctions between the
systems/approaches.

IsaPlanner is proof planner/inductive theorem prover for Isabelle. I'm
currently still working on it with Moa Johansson:

http://dream.inf.ed.ac.uk/projects/isaplanner/

We recently wrote a paper on case-splitting for rippling (2009):

http://dream.inf.ed.ac.uk/projects/isaplanner/papers/case-split-rippling-09.pdf

feedback very welcome.

Sean Wilson has recently done some work on automating inductive proofs
in Coq:

http://homepages.inf.ed.ac.uk/s0091720/
see:
Automation for Dependently Typed Functional Programming (Draft version),
To appear in: Special Issue of Fundamenta Informaticae on Dependently
Typed Programming:
http://homepages.inf.ed.ac.uk/s0091720/Wilson2009AutomationForDependentlyTypedFunctionProgramming.pdf

Other active work on inductive theorem proving is by the ACL2 community
(http://www.cs.utexas.edu/users/moore/acl2/), VeriFun
(http://www.inferenzsysteme.informatik.tu-darmstadt.de/verifun/), and
Spike (http://code.google.com/p/spike-prover/).

Hope these are useful, feel free to email me further questions, I'm
always happy to ramble about inductive proof. :)

best regards,
lucas


Razvan Voicu wrote:
> 
> Dear Coq Users,
> 
> I'm currently working on automating proofs by induction in Coq, and I
> would like to make sure I'm looking at all the relevant related work. I
> would appreciate any pointers to _recent_ work in induction automation
> (the references I get from Google are at least 5-6 years old).
> 
> Thank you in advance,
> 
> Razvan
> 
> --------------------------------------------------------
> Bug reports: http://logical.saclay.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>          http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
> 

-- 
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.