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

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

The HOL systems are not fundamentally different. There is mainly a tendency towards more frugal system infrastructure -- HOL Light is especially minimalistic.

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