*To*: Kevin Van Horn <kevin at ksvanhorn.com>*Subject*: Re: [isabelle] Theorem-proving for a Bayesian model compiler*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Wed, 16 Mar 2011 11:14:38 +0000*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <8AC639F1-C740-46CC-9F0C-C4093B16B51C@ksvanhorn.com>*References*: <8AC639F1-C740-46CC-9F0C-C4093B16B51C@ksvanhorn.com>

Mike Gordon has a snappy description of the differences between the systems: Isabelle provide a better out-of-the-box experience, while HOL is better as an API for writing code that performs inference. The various versions of HOL are much simpler internally than Isabelle, which simplifies programming. On the other hand, HOL provides less automation and its proof scripts are unintelligible. Larry Paulson On 15 Mar 2011, at 15:11, Kevin Van Horn wrote: > 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. > > Here are the features I'm looking for: > > * Interactive theorem proving (Isabelle seems to do this very well). > > * Ability to write new proof tactics. > > * 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. > > 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.) > >

**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

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