[Logiweb] Re: Larger examples?
Frederik Eriksen
frederikeriksen at get2net.dk
Wed Oct 17 15:25:17 CEST 2007
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.
More information about the Logiweb
mailing list