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 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?

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 http://isabelle.in.tum.de/documentation.html are
helpful guides.
b) had a cursory look at the existing material
http://afp.sourceforge.net/topics.shtml to get an idea how things can be
approached.

Cheers,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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