Re: [isabelle] how to create an algebra from presentation in Isabella
- To: Lee Martin CCNP <tesleft at hotmail.com>, isabelle-users <isabelle-users at cl.cam.ac.uk>
- Subject: Re: [isabelle] how to create an algebra from presentation in Isabella
- From: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>
- Date: Thu, 25 Sep 2014 16:41:12 +0200
- In-reply-to: <BAY167-W139D0A74FBC41C407F90D6AB6BE0@phx.gbl>
- Organization: TU Munich
- References: <53E4C786.email@example.com>, , , , , <alpine.LNX.firstname.lastname@example.org>, , , , , , , , <alpine.LNX.email@example.com>, , , , , <53E9F7D1.firstname.lastname@example.org>, , , , , <alpine.LNX.email@example.com>, , , , , , , , <alpine.LNX.firstname.lastname@example.org>, , , , , <53EC4820.email@example.com>, , , , , <alpine.LNX.firstname.lastname@example.org>, , , , , <email@example.com>, , , , <BAY167-W809370686657A4FE579B93B6B60@phx.gbl>, , , , <5419CAAA.firstname.lastname@example.org>, , , <BAY167-W69D8A26CD5751100F41C55B6B70@phx.gbl>, , <BAY167-W27A23559E6DDBC1A597A12B6B70@phx.gbl>, , <5423D42E.email@example.com>, <BAY167-W10731027D757803A6D8007B6BE0@phx.gbl> <BAY167-W139D0A74FBC41C407F90D6AB6BE0@phx.gbl>
- User-agent: Mozilla/5.0 (X11; Linux i686; rv:31.0) Gecko/20100101 Thunderbird/31.1.1
> 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
b) had a cursory look at the existing material
http://afp.sourceforge.net/topics.shtml to get an idea how things can be
Description: OpenPGP digital signature
This archive was generated by a fusion of
Pipermail (Mailman edition) and