# [isabelle] wikipedia entry

*To*: isabelle-users at cl.cam.ac.uk
*Subject*: [isabelle] wikipedia entry
*From*: Walther Neuper <neuper at ist.tugraz.at>
*Date*: Tue, 01 Sep 2009 18:14:59 +0200
*User-agent*: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.8.0.14eol) Gecko/20070505 Iceape/1.0.9 (Debian-1.0.13~pre080614i-0etch1)

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