Skip navigation
Use este identificador para citar ou linkar para este item: http://repositorio.unb.br/handle/10482/37158
Arquivos associados a este item:
Arquivo Descrição TamanhoFormato 
2019_DeividRodriguesdoVale.pdfDissertação787,75 kBAdobe PDFVisualizar/Abrir
Registro completo de metadados
Campo DCValorIdioma
dc.contributor.advisorNantes Sobrinho, Daniele-
dc.contributor.authorVale, Deivid Rodrigues do-
dc.date.accessioned2020-03-25T19:49:34Z-
dc.date.available2020-03-25T19:49:34Z-
dc.date.issued2020-03-25-
dc.date.submitted2019-07-26-
dc.identifier.citationVALE, Deivid Rodrigues do. Nominal disunification. 2019. 92 f. Dissertação (Mestrado em Matemática)—Universidade de Brasília, Brasília, 2019.pt_BR
dc.identifier.urihttps://repositorio.unb.br/handle/10482/37158-
dc.descriptionDissertação (mestrado)—Universidade de Brasília, Instituto de Ciências Exatas, Departamento de Matemática, 2019.pt_BR
dc.description.abstractPropõ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.pt_BR
dc.description.sponsorshipConselho Nacional de Desenvolvimento Científico e Tecnológico (CNPq).pt_BR
dc.language.isoInglêspt_BR
dc.rightsAcesso Abertopt_BR
dc.titleNominal disunificationpt_BR
dc.typeDissertaçãopt_BR
dc.subject.keywordLógica nominalpt_BR
dc.subject.keywordSemântica nominalpt_BR
dc.subject.keywordÁlgebra universalpt_BR
dc.subject.keywordDisunificaçãopt_BR
dc.subject.keywordTeoria de Disunificaçãopt_BR
dc.rights.licenseA 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.pt_BR
dc.description.abstract1An 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.pt_BR
dc.description.unidadeInstituto de Ciências Exatas (IE)pt_BR
dc.description.unidadeDepartamento de Matemática (IE MAT)pt_BR
dc.description.ppgPrograma de Pós-Graduação em Matemáticapt_BR
Aparece nas coleções:Teses, dissertações e produtos pós-doutorado

Mostrar registro simples do item Visualizar estatísticas



Os itens no repositório estão protegidos por copyright, com todos os direitos reservados, salvo quando é indicado o contrário.