# [isabelle] Theorem-proving for a Bayesian model compiler

`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.)
`

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