# [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.