• To: cl-isabelle-users at lists.cam.ac.uk
• From: Lucas Dixon <ldixon at inf.ed.ac.uk>
• Date: Tue, 09 Nov 2010 00:25:03 +0000
• User-agent: Mozilla/5.0 (Macintosh; U; Intel Mac OS X 10.6; en-US; rv:1.9.2.12) Gecko/20101027 Thunderbird/3.1.6

```Hi,

On 25/10/2010 16:55, Jasmin Christian Blanchette wrote:
```
```Now it's your turn!
```
```
Some stuff I'm involved with in Edinburgh...

Automated theory exploration:
```
We have two systems based on Isabelle/IsaPlanner which carry out automated theory exploration (IsaScheme and IsaCoSy). The idea is to see how much of in inductive theory can be generated automatically. It turns out by using counter example finding and generating only irreducible terms you get some cool stuff:
```  http://dream.inf.ed.ac.uk/projects/lemmadiscovery/
http://dream.inf.ed.ac.uk/projects/isascheme/
The IsaCoSy papers to read for this stuff are:
```
(preprint available at: http://dream.inf.ed.ac.uk/projects/isaplanner/papers/synth-ind-theories-draft-2010.pdf )
```and the IsaScheme stuff is described here:
http://dream.inf.ed.ac.uk/projects/isaplanner/papers/eswa10.pdf

An experiment using Isabelle by a working mathematician:
```
This has resulted in two things. 1) a formalization of convex analysis, (I'll let Bogdan say more about this) and 2) an "Isabelle Primer for Mathematicians" which is a quick introduction to Isabelle, highlighting some of the common difficulties and how to get around them. :)
```The Isabelle primer can be downloaded from:
http://dream.inf.ed.ac.uk/projects/isabelle/Isabelle_Primer.pdf
The formalisation will be released in due course.

Proof Planning/Inductive Theorem Proving in Isabelle:
```
we've been developing an automated inductive theorem prover (IsaPlanner). This is based on Rippling, and is primarily a research tool for exploring extensions to the technique. We've also been experimenting with proof-plan/tactic languages a bit too, and with synthesis techniques based on Isabelle's schematic variables (and machinery to manage working with them). Some info and papers are available here:
```  http://dream.inf.ed.ac.uk/projects/isaplanner/

Formalisation of Intuitionistic Linear Logic in Isabelle.
```
We've carried out various formalisations of fragments of (Intuitionistic) Linear Logic, with proof terms, in Isabelle using the nominal package, and also experimented with some other forms of handling binding (Randy Pollack can say more about this perhaps?) We really ought to tidy the linear logic stuff up and submit it to the AFP... (suddenly feeling guilty)
```
```
In the pipeline: we're hoping to provide some re-factoring tools for (Isar) proof scripts... still early days on that.
```
best,
lucas

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

```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.