[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.