[Logiweb] Re: Larger examples?

[Frederik Eriksen]

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.