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



Hi Florian,
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 axioms.is 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?
Regards,
Martin

> From: tesleft at hotmail.com
> To: florian.haftmann at informatik.tu-muenchen.de; isabelle-users at cl.cam.ac.uk
> Date: Thu, 25 Sep 2014 16:41:13 +0800
> Subject: Re: [isabelle] Is factorization mechanization for any kind of algebra?
> 
> Hi Florian,
> Thanks. i will try to use Unique Prime Factorization first.
> Regards,
> Martin
> > Date: Thu, 25 Sep 2014 10:37:02 +0200
> > From: florian.haftmann at informatik.tu-muenchen.de
> > To: tesleft at hotmail.com; isabelle-users at cl.cam.ac.uk
> > Subject: Re: [isabelle] Is factorization mechanization for any kind of	algebra?
> > 
> > Hi again,
> > 
> > > In another words, create invariant like hilbert series can classify ideals and matrix groups into different axioms.
> > > each axioms is like a Unique Prime Factorization.
> > > so is it possible to mechanize Unique Prime Factorization for different algebra and then classify these algebra's ideals or matrix group into axioms
> > 
> > well, since it seems to be a mathematical concept, you can surely
> > *formalize* it.  Since it seems to be an advanced topic were little has
> > been done so far in Isabelle/HOL, it will require a considerable amount
> > of work and is definitely nothing which I would recommend to start
> > without prior experience in Isabelle/HOL.
> > 
> > Cheers,
> > 	Florian
> > 
> > -- 
> > 
> > PGP available:
> > http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
> > 
>  		 	   		  
 		 	   		  


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