Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Announcement: Brunhilde/Rhein 2015

view this post on Zulip Email Gateway (Aug 22 2022 at 09:09):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>

the linguistic roots of Logic lie in the German speaking countries,
starting with Frege and his Begriffsschrift, followed by Gödel and many
others, so we believe that German is the natural language of choice for
creating and disseminating any formal works.

Therefore, we would like to announce the first release of a new theorem
prover:
Brunhilde 2015

One caveat: by using »Brunhilde« you are going to establish naming
conventions which are extremely difficult to give proper linguistic
foundations, esp. wrt. distangling Continental vs. Nordic origins.

As a first hint, note that the proper translation of »Sigurd« is
»Siegward«, not »Siegfried« despite some popularization by Richard Wagner.

Happy disproving,
Florian

It is fully backwards-compatible with the now legacy prover Isabelle,
but allows you to perform your proofs in the proper language for logics,
e.g.:

Satz primwurzel_irrational:
nimmt "prim (p::nat)" an
zeigt "wurzel p ∉ ℚ"
Beweis
wegen prim p gilt p: "1 < p" durch (Vereinfachung mit: prim_nat_def)
nimm "wurzel p ∈ ℚ" an
dann erhalte m n :: nat wobei
n: "n ≠ 0" und sqrt_rat: "¦wurzel p¦ = m / n"
und ggT: "ggT m n = 1" durch (Regel Rat_betrag_nat_teilt_natE)
gilt eq: "m⇧2 = p * n⇧2"
Beweis -
wegen n und sqrt_rat gilt "m = ¦wurzel p¦ * n" durch Vereinfachung
dann gilt "m⇧2 = (wurzel p)⇧2 * n⇧2"
durch (Automatismen vereinfache mit: zweierpotenz_ist_quadrat)
weiter gilt "(wurzel p)⇧2 = p" durch Vereinfachung
weiter gilt "… * n⇧2 = p * n⇧2" durch Vereinfachung
zusammengefasst zeige ?These ..
wzbw
gilt "p teilt m ∧ p teilt n"
Beweis
wegen eq gilt "p teilt m⇧2" ..
samt prim p zeige "p teilt m" durch (Regel prim_teilt_potenz_nat)
dann erhalte k wobei "m = p * k" ..
samt eq gilt "p * n⇧2 = p⇧2 * k⇧2" durch (Automatismen vereinfache mit: zweierpotenz_ist_quadrat ac_simps)
samt p gilt "n⇧2 = p * k⇧2" durch (Vereinfachung mit: zweierpotenz_ist_quadrat)
dann gilt "p teilt n⇧2" ..
samt prim p zeige "p teilt n" durch (Regel prim_teilt_potenz_nat)
wzbw
dann gilt "p teilt ggT m n" ..
samt ggT gilt "p teilt 1" durch Vereinfachung
dann gilt "p ≤ 1" durch (Vereinfachung mit: teilt_impliziert_kg)
samt p zeige Falsch durch Vereinfachung
wzbw

(Original proof due to Markus Wenzel and Tobias Nipkow.)

I have attached a proof document with the rest of the proof, and a
further example.

You can download an installable package of Brunhilde for Linux on the
Brunhilde web site, which also contains the logo, a migration guide and
a screenshot: http://pp.ipd.kit.edu/projects/brunhilde/brunhilde.php

Brunhilde is Free Software and would greatly benefit from your
contributions. Please submit any patches, hacks or work-arounds that you
came up while messing with the code at the project page on Bitbucket:
https://bitbucket.org/nomeata/brunhilde
Bug reports are also welcome there, or on any other medium of
communication (arbitrary mailing lists, twitter, Stack Exchange, reddit,
Wikipedia, personal communication or carrier pigeon).

Looking forward to your formalizations using Brunhilde/Rhein,
Joachim Breitner

signature.asc

view this post on Zulip Email Gateway (Aug 22 2022 at 09:11):

From: David Cock <david.cock@inf.ethz.ch>
Ah yes, it all started with the well-known Germanic "Logos".

David

view this post on Zulip Email Gateway (Aug 22 2022 at 09:13):

From: Makarius <makarius@sketis.net>
On the screenshot it looks like a German spell-checker is still missing.

Users of Isabelle over 20 years probably recall the introduction of
spell-checking in Isabelle2014 as one of the big landmarks in formal
document processing.

Makarius

view this post on Zulip Email Gateway (Aug 22 2022 at 09:18):

From: Makarius <makarius@sketis.net>
"Germanic" and "German" are quite different things. To understand the
German tradition of philosophy and logic, you should watch this famous
football match of 19th century Germany vs. antique Greece:
https://www.youtube.com/watch?v=ur5fGSBsfq8

Makarius

view this post on Zulip Email Gateway (Aug 22 2022 at 09:19):

From: David Cock <david.cock@inf.ethz.ch>
I'm aware of the difference, as a speaker of a non-German Germanic
language. I think it's nevertheless safe to assume that a Greek word
does not have Germanic roots. Nice video, however.

David

view this post on Zulip Email Gateway (Aug 22 2022 at 09:26):

From: "Jens-D. Doll" <jd@cococo.de>
I never laughed that loud since

'Groundhog Day',
https://www.youtube.com/watch?v=wdVKi29QWeU

in 1993!

Thanks,
Jens

view this post on Zulip Email Gateway (Aug 22 2022 at 09:40):

From: Joachim Breitner <breitner@kit.edu>
Dear Isabelle community,

the linguistic roots of Logic lie in the German speaking countries,
starting with Frege and his Begriffsschrift, followed by Gödel and many
others, so we believe that German is the natural language of choice for
creating and disseminating any formal works.

Therefore, we would like to announce the first release of a new theorem
prover:
Brunhilde 2015

It is fully backwards-compatible with the now legacy prover Isabelle,
but allows you to perform your proofs in the proper language for logics,
e.g.:

Satz primwurzel_irrational:
nimmt "prim (p::nat)" an
zeigt "wurzel p ∉ ℚ"
Beweis
wegen prim p gilt p: "1 < p" durch (Vereinfachung mit: prim_nat_def)
nimm "wurzel p ∈ ℚ" an
dann erhalte m n :: nat wobei
n: "n ≠ 0" und sqrt_rat: "¦wurzel p¦ = m / n"
und ggT: "ggT m n = 1" durch (Regel Rat_betrag_nat_teilt_natE)
gilt eq: "m⇧2 = p * n⇧2"
Beweis -
wegen n und sqrt_rat gilt "m = ¦wurzel p¦ * n" durch Vereinfachung
dann gilt "m⇧2 = (wurzel p)⇧2 * n⇧2"
durch (Automatismen vereinfache mit: zweierpotenz_ist_quadrat)
weiter gilt "(wurzel p)⇧2 = p" durch Vereinfachung
weiter gilt "… * n⇧2 = p * n⇧2" durch Vereinfachung
zusammengefasst zeige ?These ..
wzbw
gilt "p teilt m ∧ p teilt n"
Beweis
wegen eq gilt "p teilt m⇧2" ..
samt prim p zeige "p teilt m" durch (Regel prim_teilt_potenz_nat)
dann erhalte k wobei "m = p * k" ..
samt eq gilt "p * n⇧2 = p⇧2 * k⇧2" durch (Automatismen vereinfache mit: zweierpotenz_ist_quadrat ac_simps)
samt p gilt "n⇧2 = p * k⇧2" durch (Vereinfachung mit: zweierpotenz_ist_quadrat)
dann gilt "p teilt n⇧2" ..
samt prim p zeige "p teilt n" durch (Regel prim_teilt_potenz_nat)
wzbw
dann gilt "p teilt ggT m n" ..
samt ggT gilt "p teilt 1" durch Vereinfachung
dann gilt "p ≤ 1" durch (Vereinfachung mit: teilt_impliziert_kg)
samt p zeige Falsch durch Vereinfachung
wzbw

(Original proof due to Markus Wenzel and Tobias Nipkow.)

I have attached a proof document with the rest of the proof, and a
further example.

You can download an installable package of Brunhilde for Linux on the
Brunhilde web site, which also contains the logo, a migration guide and
a screenshot: http://pp.ipd.kit.edu/projects/brunhilde/brunhilde.php

Brunhilde is Free Software and would greatly benefit from your
contributions. Please submit any patches, hacks or work-arounds that you
came up while messing with the code at the project page on Bitbucket:
https://bitbucket.org/nomeata/brunhilde
Bug reports are also welcome there, or on any other medium of
communication (arbitrary mailing lists, twitter, Stack Exchange, reddit,
Wikipedia, personal communication or carrier pigeon).

Looking forward to your formalizations using Brunhilde/Rhein,
Joachim Breitner
Brunhilde-LhO-Beispiele.pdf
signature.asc

Last updated: Apr 29 2024 at 20:15 UTC