[isabelle] Announcement: Brunhilde/Rhein 2015



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


-- 
Dipl.-Math. Dipl.-Inform. Joachim Breitner
Unwissenschaftlicher Mitarbeiter
http://pp.ipd.kit.edu/~breitner

Attachment: Brunhilde-LhO-Beispiele.pdf
Description: Adobe PDF document

Attachment: signature.asc
Description: This is a digitally signed message part



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