Robert Lamar wrote:
Logiweb users,
Having worked through the tutorials (which are well-written, in my
opinion), I am now looking for other sources of information, guidance,
and inspiration as I attempt to improve my working knowledge of
Logiweb. I have found the Peano example, but it is very
foundational. Are there any examples from other parts of
mathematics? Perhaps pages which define things such as groups,
polynomials, or graphs?
As an exercise for myself, I am attempting to define a bit of ring
theory in the system, and would be grateful for pointers to models and
other documentation which may exist. While the tutorials were a good
introduction to the flavor of the system, the examples there are quite
small.
Thanks in advance for your help.
Robert
Hi Robert,
Well, there is my M.Sc. thesis "Constructing the real numbers in
Logiweb" (URL: www.topps.diku.dk/eriksen/realNumbers). In the thesis, I
develop some of Cantor's theory of the real numbers, using ZF set theory
(and propositional logic and predicate logic). A word of caution: Most
of the thesis is in Danish. However, since the formal theorems of the
thesis are in English, it may still be of some use to you.
Best regards
Frederik.
_______________________________________________
Logiweb mailing list
Logiweb@diku.dk
http://lists.diku.dk/mailman/listinfo/logiweb
(Web access from inside DIKUs LAN only)