*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.5050909@inf.ethz.ch>, , , , , <alpine.LNX.2.00.1408081536350.13355@lxbroy10.informatik.tu-muenchen.de>, , , , , , , , <alpine.LNX.2.00.1408091309180.35652@lxbroy10.informatik.tu-muenchen.de>, , , , , <53E9F7D1.9060409@inf.ethz.ch>, , , , , <alpine.LNX.2.00.1408131707001.27833@lxbroy10.informatik.tu-muenchen.de>, , , , , , , , <alpine.LNX.2.00.1408131723130.29642@lxbroy10.informatik.tu-muenchen.de>, , , , , <53EC4820.7000304@inf.ethz.ch>, , , , , <alpine.LNX.2.00.1408181323070.16628@lxbroy10.informatik.tu-muenchen.de>, , , , , <54184884.60005@inf.ethz.ch>, , , , <BAY167-W809370686657A4FE579B93B6B60@phx.gbl>, , , , <5419CAAA.2010401@informatik.tu-muenchen.de>, , , <BAY167-W69D8A26CD5751100F41C55B6B70@phx.gbl>, , <BAY167-W27A23559E6DDBC1A597A12B6B70@phx.gbl>, , <5423D42E.5070208@informatik.tu-muenchen.de>, <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

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

**References**:**Re: [isabelle] Isabelle2014-RC2: PIDE does not resume processing***From:*Andreas Lochbihler

**[isabelle] Is factorization mechanization for any kind of algebra?***From:*Lee Martin CCNP

**Re: [isabelle] Is factorization mechanization for any kind of algebra?***From:*Florian Haftmann

**Re: [isabelle] Is factorization mechanization for any kind of algebra?***From:*Lee Martin CCNP

**Re: [isabelle] Is factorization mechanization for any kind of algebra?***From:*Lee Martin CCNP

**Re: [isabelle] Is factorization mechanization for any kind of algebra?***From:*Florian Haftmann

**Re: [isabelle] Is factorization mechanization for any kind of algebra?***From:*Lee Martin CCNP

**[isabelle] how to create an algebra from presentation in Isabella***From:*Lee Martin CCNP

- Previous by Date: [isabelle] QED+20 - JFR Special Issue: Call for Papers
- Next by Date: [isabelle] Code Generator and export of functions in Haskell
- Previous by Thread: [isabelle] how to create an algebra from presentation in Isabella
- Next by Thread: [isabelle] Lemma pos_mod_bound
- Cl-isabelle-users September 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list