Re: [isabelle] how to create an algebra from presentation in Isabella

Hi Martin,

> i find a book called topology via logic, which mentioned T algebra is
presented by T<generators | relation>
> is it true?is there an example about this?
> I do not know what will be done after prove an algebra.are the axioms that will be written into another language which has rewriting, for calculation of for example addition and multiplication?then, what is the usage after this?
> I just understand that to create some invariants to classify ideals into it further work is for classification of ideals into axioms which is topological space which is frame which is a distributive lattice that all combination subset (a,b) having <= .  and each having common lower node and common upper node?

honestly, I am neither an expert in algebra nor topology.

This mailing list is medium of exchange between users of Isabelle, and
if you expect answers you should boil down your questions in a suitable
manner related to the system. This requires that you have
a) spent some time get acquainted with the basics of the system itself,
ie. written some simple specifications and proofs yourself. The first
two tutorials at are
helpful guides.
b) had a cursory look at the existing material to get an idea how things can be



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.