[isabelle] wikipedia entry



Dear list members,

from time to time having discussions with "pure mathematicians" (i.e.
mathematicians who don't take computers serious beyond LaTeX) about
computer theorem proving (CTP), I would welcome wikipedias entry on
Isabelle supporting arguments like these:

# CTP represents mathematical knowledge in (almost) traditional notation
# CTP, in particular Isar, represents proofs in (almost) traditional
notation
... both representations can be read by humans as well as be interpreted by machines, and thus CTP is a straight-forward continuation in the tradition of pure mathematics (... might well be weakened ;-)

With respect to the standard reader of wikipedia, doesn't the present
article emphasize technicalities too much ? Wouldn't be information more appropriate like: # representation of mathematical knowledge, e.g. introducing [[integer]]s based on [[natural number]]s:
    definition intrel :: "((nat × nat) × (nat × nat)) set" where
    [code del]: "intrel = {((x, y), (u, v)) | x y u v. x + v = u + y }"
    with examples even for non-mathematicians:
      ((3, 1), (4, 2)) | 3 + 2 = 1 + 4 ,
      ((3, 1), (5, 3)) | 3 + 3 = 1 + 5 ,
      ((3, 1), (6, 4)) | 3 + 4 = 1 + 6 , ...
    i.e. (3, 1) \equiv (4, 2) \equiv (5, 3) \equiv (6, 4) \equiv ...
    where this [[equivalence class]] is written as [[integer]] "-2"
# representation of proofs: Shouldn't the outdated "programing style" proof be replaced by an example for an Isar proof (while there might be better examples than the one addressed by the link "declarative proof style") ?

Is somebody out there, who is unsatisfied with the present article _and_ expert enough to make an acknowledged revision ?

Walther
--
------------------------------------------------------------------------
Walther Neuper                          Mailto: neuper at ist.tugraz.at
Institute for Software Technology          Tel: +43-(0)316/873-5728
University of Technology                   Fax: +43-(0)316/873-5706
Graz, Austria                             Home: www.ist.tugraz.at/neuper
------------------------------------------------------------------------






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