Nominal commutative narrowing
Furkejuvvon:
| Váldodahkki: | |
|---|---|
| Almmustuhttinbeaivi: | 2022 |
| Materiálatiipa: | Master thesis |
| Giella: | por |
| Gáldu: | Repositório Institucional da UnB |
| Download full: | https://repositorio.unb.br/handle/10482/44597 |
Čoahkkáigeassu: | Dissertação (mestrado) — Universidade de Brasília, Instituto de Ciências Exatas, Departamento de Matemática, 2022. |
| _version_ | 1871442380182257664 |
|---|---|
| author | Souza, Daniella Santaguida Magalhães de |
| author_browse | Souza, Daniella Santaguida Magalhães de |
| author_facet | Souza, Daniella Santaguida Magalhães de |
| author_role | author |
| bitstream.checksum.fl_str_mv | 4b9bb56a1142cac03aae0cd7e77ddb64 bacfee268cc5d4f6aaa2e6e0066d38f5 |
| bitstream.checksumAlgorithm.fl_str_mv | MD5 MD5 |
| bitstream.url.fl_str_mv | http://repositorio.unb.br/bitstream/10482/44597/1/2022_DaniellaSantaguidaMagalh%c3%a3esdeSouza.pdf http://repositorio.unb.br/bitstream/10482/44597/2/license.txt |
| collection | Repositório Institucional da UnB |
| contributor_str_mv | Nantes Sobrinho, Daniele |
| dc.contributor.advisor1.fl_str_mv | Nantes Sobrinho, Daniele |
| dc.contributor.author.fl_str_mv | Souza, Daniella Santaguida Magalhães de |
| dc.contributor.email.pt_BR.fl_str_mv | dani.sms@hotmail.com |
| dc.date.accessioned.fl_str_mv | 2022-08-20T21:25:17Z |
| dc.date.available.fl_str_mv | 2022-08-20T21:25:17Z |
| dc.date.issued.fl_str_mv | 2022-08-20 |
| dc.date.submitted.none.fl_str_mv | 2022-06-07 |
| dc.identifier.citation.fl_str_mv | SOUZA, Daniella Santaguida Magalhães de. Grupos finitos com poucos elementos em órbitas por automorfismos. 2022. 80 f., il. Dissertação (Mestrado em Matemática) — Universidade de Brasília, Brasília, 2022. |
| dc.identifier.uri.fl_str_mv | https://repositorio.unb.br/handle/10482/44597 |
| dc.language.iso.fl_str_mv | por |
| dc.rights.driver.fl_str_mv | info:eu-repo/semantics/openAccess |
| dc.source.none.fl_str_mv | reponame:Repositório Institucional da UnB instname:Universidade de Brasília (UnB) instacron:UNB |
| dc.subject.keyword.pt_BR.fl_str_mv | Modelagem Raciocínio equacional Técnicas de reescrita Lógica nominal |
| dc.title.pt_BR.fl_str_mv | Nominal commutative narrowing |
| dc.type.driver.fl_str_mv | info:eu-repo/semantics/masterThesis |
| dc.type.status.fl_str_mv | info:eu-repo/semantics/publishedVersion |
| description | Dissertação (mestrado) — Universidade de Brasília, Instituto de Ciências Exatas, Departamento de Matemática, 2022. |
| eu_rights_str_mv | openAccess |
| format | masterThesis |
| id | UNB_7fdb2ceca299e305569b404a5c8be0f0 |
| identifier_str_mv | SOUZA, Daniella Santaguida Magalhães de. Grupos finitos com poucos elementos em órbitas por automorfismos. 2022. 80 f., il. Dissertação (Mestrado em Matemática) — Universidade de Brasília, Brasília, 2022. |
| instacron_str | UNB |
| institution | UNB |
| instname_str | Universidade de Brasília (UnB) |
| language | por |
| network_acronym_str | UNB |
| network_name_str | Repositório Institucional da UnB |
| oai_identifier_str | oai:repositorio.unb.br:10482/44597 |
| publishDate | 2022 |
| publishDateSort | 2022 |
| reponame_str | Repositório Institucional da UnB |
| repository.mail.fl_str_mv | repositorio@unb.br |
| repository.name.fl_str_mv | Repositório Institucional da UnB - Universidade de Brasília (UnB) |
| repository_id_str | |
| spelling | Souza, Daniella Santaguida Magalhães dedani.sms@hotmail.comNantes Sobrinho, Daniele2022-08-20T21:25:17Z2022-08-20T21:25:17Z2022-08-202022-06-07SOUZA, Daniella Santaguida Magalhães de. Grupos finitos com poucos elementos em órbitas por automorfismos. 2022. 80 f., il. Dissertação (Mestrado em Matemática) — Universidade de Brasília, Brasília, 2022.https://repositorio.unb.br/handle/10482/44597Dissertação (mestrado) — Universidade de Brasília, Instituto de Ciências Exatas, Departamento de Matemática, 2022.Modelagem e raciocínio equacional são onipresentes na Matemática e na Ciência da Computação. Técnicas de reescrita têm sido aplicadas com sucesso para formalizar e implementar inferência automatizada em estruturas matemáticas dedutivas. Apresentar teorias equacionais por meio da reescrita dá origem a um mecanismo para decidir a redução equacional da teoria sempre que o sistema de reescrita for terminante e confluente, ou seja, sempre que for convergente. Resolver problemas equacionais é um passo adiante que requer mais esforço do que apenas usar reescrita. De fato, “estreitar” problemas equacionais é uma técnica bem conhecida que adiciona à reescrita o poder necessário para buscar soluções; em outras palavras, adiciona o poder de buscar instâncias das variáveis que ocorrem em um problema equacional que “unifica” as equações. Por sua vez, a lógica nominal foi desenvolvida para contornar as inconveniências apresentadas quando as variáveis são instanciadas. A abordagem nominal usa átomos nominais em vez de variáveis para evitar a necessidade de renomeação de variáveis ao lidar com equações na abordagem notacional padrão. A sintaxe nominal também inclui permutações de átomos para distinguir algebricamente os átomos evitando colisões e capturas destes. Neste trabalho, estudamos a reescrita nominal módulo comutatividade. Desenvolvemos o método estreitamento nominal comutativo (nominal commutative narrowing) para lidar com o problema de unificação nominal módulo teorias equacionais que incluem comutatividade, o qual não é finitário dependendo da representação das soluções.Equational modelling and reasoning are ubiquitous in Mathematics and Computer Science. Rewriting techniques have been applied successfully to formalize and implement automated inference in mathematical deductive frameworks. Presenting equational theories by rewriting gives rise to a mechanism to decide the equational reduct of the theory whenever the rewriting system is terminating and confluent, i.e., whenever it is convergent. Solving equational problems is a step further that requires more effort than just rewriting. Indeed, “narrowing” equational problems is a well-known technique that adds to rewriting the required power to search for solutions; in other words, it adds the power to search for instantiations of the variables occurring in an equational problem that “unify” the equations. On its side, the nominal logic has been developed to contour inconveniences presented when variables are instantiated. The nominal approach uses nominal atoms instead of variables to avoid the requirement of variable renaming when dealing with equations in the standard notational approach. The nominal syntax also includes atom permutations to algebraically distinguish atoms avoiding atom collisions and captures. In this work, we study nominal rewriting modulo commutativity. We develop nominal commutative narrowing to deal with the problem of nominal unification modulo equational theories that include commutativity, which is not finitary depending on the representation of solutions.Instituto de Ciências Exatas (IE)Departamento de Matemática (IE MAT)Programa de Pós-Graduação em MatemáticaporA concessão da licença deste item refere-se ao termo de autorização impresso assinado pelo autor com as seguintes condições: Na qualidade de titular dos direitos de autor da publicação, autorizo a Universidade de Brasília e o IBICT a disponibilizar por meio dos sites www.bce.unb.br, www.ibict.br, http://hercules.vtls.com/cgi-bin/ndltd/chameleon?lng=pt&skin=ndltd sem ressarcimento dos direitos autorais, de acordo com a Lei nº 9610/98, o texto integral da obra disponibilizada, conforme permissões assinaladas, para fins de leitura, impressão e/ou download, a título de divulgação da produção científica brasileira, a partir desta data.info:eu-repo/semantics/openAccessNominal commutative narrowinginfo:eu-repo/semantics/publishedVersioninfo:eu-repo/semantics/masterThesisModelagemRaciocínio equacionalTécnicas de reescritaLógica nominalreponame:Repositório Institucional da UnBinstname:Universidade de Brasília (UnB)instacron:UNBORIGINAL2022_DaniellaSantaguidaMagalhãesdeSouza.pdf2022_DaniellaSantaguidaMagalhãesdeSouza.pdfapplication/pdf1373982http://repositorio.unb.br/bitstream/10482/44597/1/2022_DaniellaSantaguidaMagalh%c3%a3esdeSouza.pdf4b9bb56a1142cac03aae0cd7e77ddb64MD51open accessLICENSElicense.txtlicense.txttext/plain671http://repositorio.unb.br/bitstream/10482/44597/2/license.txtbacfee268cc5d4f6aaa2e6e0066d38f5MD52open access10482/445972025-03-19 12:52:26.643open accessoai:repositorio.unb.br:10482/44597QSBjb25jZXNzw6NvIGRhIGxpY2Vuw6dhIGRlc3RlIGl0ZW0gcmVmZXJlLXNlIGFvIHRlcm1vIGRlIGF1dG9yaXphw6fDo28gaW1wcmVzc28gYXNzaW5hZG8gDQpwZWxvIGF1dG9yIGNvbSBhcyBzZWd1aW50ZXMgY29uZGnDp8O1ZXM6DQoNCk5hIHF1YWxpZGFkZSBkZSB0aXR1bGFyIGRvcyBkaXJlaXRvcyBkZSBhdXRvciBkYSBwdWJsaWNhw6fDo28sIGF1dG9yaXpvIGEgVW5pdmVyc2lkYWRlIGRlIEJyYXPDrWxpYQ0KIGUgbyBJQklDVCBhIGRpc3BvbmliaWxpemFyIHBvciBtZWlvIGRvcyBzaXRlcyB3d3cuYmNlLnVuYi5iciwgd3d3LmliaWN0LmJyLA0KIGh0dHA6Ly9oZXJjdWxlcy52dGxzLmNvbS9jZ2ktYmluL25kbHRkL2NoYW1lbGVvbj9sbmc9cHQmc2tpbj1uZGx0ZCBzZW0gcmVzc2FyY2ltZW50byBkb3MgDQpkaXJlaXRvcyBhdXRvcmFpcywgZGUgYWNvcmRvIGNvbSBhIExlaSBuwrogOTYxMC85OCwgbyB0ZXh0byBpbnRlZ3JhbCBkYSBvYnJhIGRpc3BvbmliaWxpemFkYSwNCiBjb25mb3JtZSBwZXJtaXNzw7VlcyBhc3NpbmFsYWRhcywgcGFyYSBmaW5zIGRlIGxlaXR1cmEsIGltcHJlc3PDo28gZS9vdSBkb3dubG9hZCwgYSB0w610dWxvIGRlIA0KZGl2dWxnYcOnw6NvIGRhIHByb2R1w6fDo28gY2llbnTDrWZpY2EgYnJhc2lsZWlyYSwgYSBwYXJ0aXIgZGVzdGEgZGF0YS4=Repositório InstitucionalPUBhttps://repositorio.unb.br/oai/requestrepositorio@unb.bropendoar:2025-03-19T15:52:26Repositório Institucional da UnB - Universidade de Brasília (UnB) |
| spellingShingle | Nominal commutative narrowing Souza, Daniella Santaguida Magalhães de Modelagem Raciocínio equacional Técnicas de reescrita Lógica nominal |
| status_str | publishedVersion |
| title | Nominal commutative narrowing |
| title_full | Nominal commutative narrowing |
| title_fullStr | Nominal commutative narrowing |
| title_full_unstemmed | Nominal commutative narrowing |
| title_short | Nominal commutative narrowing |
| title_sort | Nominal commutative narrowing |
| topic | Modelagem Raciocínio equacional Técnicas de reescrita Lógica nominal |
| url | https://repositorio.unb.br/handle/10482/44597 |