Re: [isabelle] Theorem-proving for a Bayesian model compiler
On Tue, 15 Mar 2011, Kevin Van Horn wrote:
* 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.
It is not as simple as I would like it to have, but it works, and people
have done it before, e.g. in the Isabelle/TLA+ IDE. (The technology for
Isabelle integration is about to change substantially in the coming
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
The HOL systems are not fundamentally different. There is mainly a
tendency towards more frugal system infrastructure -- HOL Light is
The main alternative to Isabelle is actually Coq, but there are quite
different logical foundations, and less system manuals.
This archive was generated by a fusion of
Pipermail (Mailman edition) and