*To*: Kevin Van Horn <kevin at ksvanhorn.com>*Subject*: Re: [isabelle] Theorem-proving for a Bayesian model compiler*From*: Johannes Hölzl <hoelzl at in.tum.de>*Date*: Wed, 16 Mar 2011 11:14:33 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <8AC639F1-C740-46CC-9F0C-C4093B16B51C@ksvanhorn.com>*Organization*: Technische Universität München*References*: <8AC639F1-C740-46CC-9F0C-C4093B16B51C@ksvanhorn.com>

Am Dienstag, den 15.03.2011, 09:11 -0600 schrieb Kevin Van Horn: > I'm trying to figure out if Isabelle is the right theorem prover / > proof assistant for my needs, or if I should use something else. I'm > writing a Bayesian model compiler, something that will turn a > specification of a joint probability distribution plus indication of > what variables are observed into Markov chain Monte Carlo code for > estimating the parameters. There are existing software packages that > do something similar -- WinBUGS/OpenBUGS, JAGS, and hbc -- but they > all have limitations that are unacceptable for my purposes, and it > appears that I'll need some sort of theorem proving to overcome those > limitations. Which mathematical background theories do you need? We have measure / probability theory but no theorems about MCMC. > Here are the features I'm looking for: > > * Interactive theorem proving (Isabelle seems to do this very well). > * Ability to write new proof tactics. I only developed two small tactics in Isabelle, so I'm not very experienced. But I think it is very easy to do in the interactive mode in ProofGeneral. Open a new theory and write theory test imports Main begin ML {* fun ..... *} theorem "..." apply (tactic {* ML code *}) This is a very nice playground for ideas, later you can of course move your code to its own ML-file. A introduction on how to write tactics is found in the Isabelle Cookbook: http://www4.in.tum.de/~urbanc/cgi-bin/repos.cgi/isabelle-cookbook/raw-file/tip/progtutorial.pdf For further information take a look at the reference manuals http://isabelle.in.tum.de/documentation.html > * Ability to do derivational proofs where I know the form of what I > want to prove but don't know exactly what I'm proving until I reach > the end. For example, I'm doing a chain of A1 = A2 = ... An, and only > when I reach an An that has the form I want do I know I'm done and > know that A1 = An is what I'm proving. Likewise, I might be trying to > find a usable upper bound: B1 <= B2 <= ... Bn. > * Ability to call the theorem prover as a software module in a larger > system (no user interaction). This would be for tasks simple enough to > fully automate with appropriate tactics, or to spit out subgoals for > which the user will need to provide proofs in harder cases. Some proof methods in Isabelle work in this way. The most often used proof method (simp) works in this way. The user states a goal, applies the simplifier and gets back the simplified goal where he can apply further tactics. (This should also answer the previous question.) > How does Isabelle rate on these? Would a different theorem prover / > proof assistant better fill these requirements? > > (BTW I'm also looking at HOL Light and HOL 4, which appear have the > last three features above, but my impression is that Isabelle is > easier to use for interactive proof and that the finished proofs are > easier to read.) I have no experiences with HOL Light or HOL 4. When you write your proofs in Isar (Isabelle's proof language) they are more readable. However I assume the OCaml / ML internals of HOL Light / HOL 4 are easier to understand. Greetings, Johannes

**Follow-Ups**:**Re: [isabelle] Theorem-proving for a Bayesian model compiler***From:*Kevin Van Horn

**References**:**[isabelle] Theorem-proving for a Bayesian model compiler***From:*Kevin Van Horn

- Previous by Date: [isabelle] Theorem-proving for a Bayesian model compiler
- Next by Date: Re: [isabelle] Theorem-proving for a Bayesian model compiler
- Previous by Thread: [isabelle] Theorem-proving for a Bayesian model compiler
- Next by Thread: Re: [isabelle] Theorem-proving for a Bayesian model compiler
- Cl-isabelle-users March 2011 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list