*To*: Johannes Hölzl <hoelzl at in.tum.de>*Subject*: Re: [isabelle] Theorem-proving for a Bayesian model compiler*From*: Kevin Van Horn <kevin at ksvanhorn.com>*Date*: Wed, 16 Mar 2011 09:24:20 -0600*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <1300270473.2260.82.camel@macbroy12.informatik.tu-muenchen.de>*References*: <8AC639F1-C740-46CC-9F0C-C4093B16B51C@ksvanhorn.com> <1300270473.2260.82.camel@macbroy12.informatik.tu-muenchen.de>

On Mar 16, 2011, at 4:14 AM, Johannes Hölzl wrote:

Am Dienstag, den 15.03.2011, 09:11 -0600 schrieb Kevin Van Horn:... I'm writing a Bayesian model compiler, something that willturn aspecification of a joint probability distribution plus indication of what variables are observed into Markov chain Monte Carlo code forestimating the parameters. ... it appears that I'll need some sortof theorem proving...Which mathematical background theories do you need? We have measure / probability theory but no theorems about MCMC.

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

-- Kevin

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

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

**Re: [isabelle] Theorem-proving for a Bayesian model compiler***From:*Johannes Hölzl

- Previous by Date: Re: [isabelle] How do I make notation work only on the constant instead of on the type as well?
- Next by Date: Re: [isabelle] Theorem-proving for a Bayesian model compiler
- Previous by Thread: Re: [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