[isabelle] Advertise your work on the mailing list
This is just a reminder that we are all encouraged to let the mailing list know about your Isabelle-based work on the mailing list. This is especially important if you publish your work elsewhere than at the ITP conference or on the Archive of Formal Proof. Other people on the mailing list might be doing something similar without knowing. (This happened recently with an Isabelle-related paper presented at LPAR.)
Three Years of Experience with Sledgehammer, a Practical Link between Automatic and Interactive Theorem Provers
w/ Lawrence C. Paulson
IWIL 2010 (Yogyakarta, Indonesia)
Sledgehammer is a highly successful subsystem of Isabelle/HOL that calls automatic theorem provers to assist with interactive proof construction. It requires no user configuration: it can be invoked with a single mouse gesture at any point in a proof. It automatically finds relevant lemmas from all those currently available. An unusual aspect of its architecture is its use of unsound translations, coupled with its delivery of results as Isabelle/HOL proof scripts: its output cannot be trusted, but it does not need to be trusted. Sledgehammer works well with Isar structured proofs and allows beginners to prove challenging theorems.
Now it's your turn!
This archive was generated by a fusion of
Pipermail (Mailman edition) and