Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] canonical citations for Isabelle/HOL and Sledg...

Email Gateway (Sep 13 2022 at 00:15):

From: Yutaka Nagashima <united.reasoning@gmail.com>
Dear list,

Do we have canonical citations for Isabelle/HOL and Sledgehammer?

For Isabelle/HOL, I used to cite the old tutorial "A Proof Assistant for
Higher-Order Logic".
However, this tutorial is now officially declared as an "Old Isabelle
Manual" at isabelle.in.tum.de.

For Sledgehammer, I thought of "Hammering towards QED" at JAR as the
canonical citation.
But "Seventeen Provers Under the Hammer" contains more recent results.

Let me know what you think and prefer.

Regards,
Yutaka

Email Gateway (Sep 13 2022 at 07:44):

From: Tobias Nipkow <nipkow@in.tum.de>
On 13/09/2022 02:15, Yutaka Nagashima wrote:

Dear list,

Do we have canonical citations for Isabelle/HOL and Sledgehammer?

For Isabelle/HOL, I used to cite the old tutorial "A Proof Assistant for
Higher-Order Logic".
However, this tutorial is now officially declared as an "Old Isabelle Manual" at
isabelle.in.tum.de <http://isabelle.in.tum.de>.

I think this is still a good work to cite for historic reasons. You could
additionally cite the Reference manual or Part I of Concrete Semantics depending
on what you want to emphasize.

Tobias

For Sledgehammer, I thought of "Hammering towards QED" at JAR as the canonical
citation.
But "Seventeen Provers Under the Hammer" contains more recent results.

Let me know what you think and prefer.

Regards,
Yutaka
smime.p7s

Email Gateway (Sep 13 2022 at 21:01):

From: Yutaka Nagashima <united.reasoning@gmail.com>
Thank you!
I will cite them accordingly.

Regards,
Yutaka

Last updated: Jan 04 2025 at 20:18 UTC