Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] how to create an algebra from presentation in ...


view this post on Zulip Email Gateway (Aug 19 2022 at 15:54):

From: Lee Martin CCNP <tesleft@hotmail.com>
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


Last updated: Apr 19 2024 at 16:20 UTC