[mizar] Masters thesis - Case studies in Mizar and Coq

[rk1 <rkam2001@hotmail.com>]

Dear Mizar community,

Hope your Mizar endeavors are going well.

My advisor Dr. Beeson has graciously posted a link to the master's thesis
that he advised me on.  The link from his homepage is
http://www.cs.sjsu.edu/faculty/beeson/Masters/KamThesis.pdf.  It may be
useful to those interested in a new user's experience learning Mizar (and
compared to the Coq system), or interested in proofs of a group theory
result (the orbit-stabilizer theorem) and/or Markov's inequality.  It has
some figures for how long it takes a new user to write proofs in Mizar.  The
second half of the paper discusses tricky parts of Mizar that took me a
while to figure out, some of which are already fixed in the newest Mizar
release.

Best wishes,
Robert

P.S. Thanks for the advice on the RELPREM/RELINFER issue which I used to
complete the submission of the proofs to the MML committee.
-- 
View this message in context: http://www.nabble.com/Masters-thesis---Case-studies-in-Mizar-and-Coq-tp15116441p15116441.html
Sent from the Mizar mailing list archive at Nabble.com.