Atenção: Todas as denúncias são sigilosas e sua identidade será preservada.
Os campos nome e e-mail são de preenchimento opcional
Metadados | Descrição | Idioma |
---|---|---|
Autor(es): dc.contributor | Nantes Sobrinho, Daniele | - |
Autor(es): dc.contributor | dani.sms@hotmail.com | - |
Autor(es): dc.creator | Souza, Daniella Santaguida Magalhães de | - |
Data de aceite: dc.date.accessioned | 2024-07-22T11:58:39Z | - |
Data de disponibilização: dc.date.available | 2024-07-22T11:58:39Z | - |
Data de envio: dc.date.issued | 2022-08-20 | - |
Data de envio: dc.date.issued | 2022-08-20 | - |
Data de envio: dc.date.issued | 2022-08-20 | - |
Data de envio: dc.date.issued | 2022-06-07 | - |
Fonte completa do material: dc.identifier | https://repositorio.unb.br/handle/10482/44597 | - |
Fonte: dc.identifier.uri | http://educapes.capes.gov.br/handle/capes/793286 | - |
Descrição: dc.description | Dissertação (mestrado) — Universidade de Brasília, Instituto de Ciências Exatas, Departamento de Matemática, 2022. | - |
Descrição: dc.description | 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. | - |
Descrição: dc.description | 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. | - |
Descrição: dc.description | Instituto de Ciências Exatas (IE) | - |
Descrição: dc.description | Departamento de Matemática (IE MAT) | - |
Descrição: dc.description | Programa de Pós-Graduação em Matemática | - |
Formato: dc.format | application/pdf | - |
Direitos: dc.rights | Acesso Aberto | - |
Direitos: dc.rights | A 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. | - |
Palavras-chave: dc.subject | Modelagem | - |
Palavras-chave: dc.subject | Raciocínio equacional | - |
Palavras-chave: dc.subject | Técnicas de reescrita | - |
Palavras-chave: dc.subject | Lógica nominal | - |
Título: dc.title | Nominal commutative narrowing | - |
Aparece nas coleções: | Repositório Institucional – UNB |
O Portal eduCAPES é oferecido ao usuário, condicionado à aceitação dos termos, condições e avisos contidos aqui e sem modificações. A CAPES poderá modificar o conteúdo ou formato deste site ou acabar com a sua operação ou suas ferramentas a seu critério único e sem aviso prévio. Ao acessar este portal, você, usuário pessoa física ou jurídica, se declara compreender e aceitar as condições aqui estabelecidas, da seguinte forma: