Re: [isabelle] Announcement: Brunhilde/Rhein 2015



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

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.