http://repositorio2.unb.br/jspui/handle/10482/37158| Arquivo | Descrição | Tamanho | Formato | |
|---|---|---|---|---|
| 2019_DeividRodriguesdoVale.pdf | Dissertação | 787,75 kB | Adobe PDF | Visualizar/Abrir |
| Título: | Nominal disunification |
| Autor(es): | Vale, Deivid Rodrigues do |
| Orientador(es): | Nantes Sobrinho, Daniele |
| Assunto: | Lógica nominal Semântica nominal Álgebra universal Disunificação Teoria de Disunificação |
| Data de publicação: | 25-Mar-2020 |
| Data de defesa: | 26-Jul-2019 |
| Referência: | VALE, Deivid Rodrigues do. Nominal disunification. 2019. 92 f. Dissertação (Mestrado em Matemática)—Universidade de Brasília, Brasília, 2019. |
| Resumo: | Propõe-se uma extensão para problemas de disunificação de primeira-ordem adicionando suporte a operadores de ligação de acordo com a abordagem nominal. Nesta abordagem, abstração é implementada usando átomos nominais ao invés de variáveis de ligação como na representação clássica de termos e renomeamento de átomos é implementado por permutações. Em lógica nominal problemas de unificação consistem de perguntas equacionais da forma s ≈α ? t (lê-se: s é α-equivalente a t?) consideradas sobre problemas de freshness da forma a# ? t (lê-se: a é fresco em t?) que restringem soluções proibindo ocorrências livres de átomos na instanciação de variáveis. Além dessas questões equacionais e freshness, problemas de disunificação nominal incluem restrições na forma de disequações s ̸≈α ? t (lê-se: s é αdiferente de t?) com soluções dadas por pares consistindo de uma substituição σ e um conjunto de restrições de freshness na forma a#X tal que sobre estas restrições a σ-instanciação de equações, disequações, e problemas de freshness são válidas. Mostra-se, reutilizando noções de unificação nominal, como decidir se dois termos nominais podem ser feitos diferentes módulo α-equivalência. Isso é feito extendendo resultados anteriores sobre disunificação de primeira ordem e definindo a noção de soluções com exceção na linguagem nominal. Uma discussão sobre a semântica de restrições em forma de disequações também é apresentada. |
| Abstract: | An extension of first-order disunification problems is proposed by taking into account binding operators according to the nominal approach. In this approach, bindings are implemented through nominal atoms used instead of binding variables and renaming of atoms are implemented by atom permutations. In the nominal setting, unification problems consist of equational questions of the form s ≈α ? t (read: is s α-equivalent to t?) considered under freshness problems a# ? t (read: is a fresh for t?) that restrict solutions by forbidding free occurrences of atoms in the instantiations of variables. In addition to equational and freshness problems, nominal disunification problems also include nominal disunification constraints in the form of disequations s ̸≈α ? t (read: is s α-different to t?) and their solutions consist of pairs of a substitution σ and a finite set of freshness constraints in the form of a#X such that under these restrictions the σ-instantiation of the equations, disequations, and freshness problems holds. By re-using nominal unification techniques, it is shown how to decide whether two nominal terms can be made different modulo α-equivalence. This is done by extending previous results on first-order disunification and by defining the notion of solutions with exceptions in the nominal syntax. A discussion on the semantics of disunification constraints is also given. |
| Unidade Acadêmica: | Instituto de Ciências Exatas (IE) Departamento de Matemática (IE MAT) |
| Informações adicionais: | Dissertação (mestrado)—Universidade de Brasília, Instituto de Ciências Exatas, Departamento de Matemática, 2019. |
| Programa de pós-graduação: | Programa de Pós-Graduação em Matemática |
| Licença: | 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. |
| Agência financiadora: | Conselho Nacional de Desenvolvimento Científico e Tecnológico (CNPq). |
| Aparece nas coleções: | Teses, dissertações e produtos pós-doutorado |
Os itens no repositório estão protegidos por copyright, com todos os direitos reservados, salvo quando é indicado o contrário.