[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

More information about the Logiweb mailing list