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