| DC Field | Value | Language |
|---|
| dc.contributor.author | Ayala-Rincón, Mauricio | - |
| dc.contributor.author | Fernández, Maribel | - |
| dc.contributor.author | Nantes Sobrinho, Daniele | - |
| dc.date.accessioned | 2019-06-11T14:31:32Z | - |
| dc.date.available | 2019-06-11T14:31:32Z | - |
| dc.date.issued | 2018 | - |
| dc.identifier.citation | AYALA-RINCÓN, Mauricio; FERNÁNDEZ, Maribel; NANTES SOBRINHO, Daniele. Fixed-point constraints for nominal equational unification. In: INTERNATIONAL CONFERENCE ON FORMAL STRUCTURES FOR COMPUTATION AND DEDUCTION, 3., 2018, Dagstuhl - Germany. Proceedings [...]. Dagstuhl - Germany: Daugstuhl research Online Publishing Server, 2018. DOI: 10.4230/LIPIcs.FSCD.2018.7. Disponível em: http://drops.dagstuhl.de/opus/volltexte/2018/9177/. Acesso em: 11 jun. 2019. | pt_BR |
| dc.identifier.uri | http://repositorio.unb.br/handle/10482/34780 | - |
| dc.language.iso | Inglês | pt_BR |
| dc.publisher | Daugstuhl research Online Publishing Server | pt_BR |
| dc.rights | Acesso Aberto | pt_BR |
| dc.title | Fixed-point constraints for nominal equational unification | pt_BR |
| dc.type | Trabalho apresentado em evento | pt_BR |
| dc.subject.keyword | Termos nominais | pt_BR |
| dc.subject.keyword | Equações de ponto fixo | pt_BR |
| dc.subject.keyword | Unificação nominal | pt_BR |
| dc.subject.keyword | Teoria de equações | pt_BR |
| dc.rights.license | © Mauricio Ayala-Rincón, Maribel Fernández, and Daniele Nantes-Sobrinho; licensed under Creative Commons License CC-BY. | pt_BR |
| dc.identifier.doi | 10.4230/LIPIcs.FSCD.2018.7 | pt_BR |
| dc.description.abstract1 | We propose a new axiomatisation of the alpha-equivalence relation for nominal terms, based on a
primitive notion of fixed-point constraint. We show that the standard freshness relation between
atoms and terms can be derived from the more primitive notion of permutation fixed-point, and
use this result to prove the correctness of the new alpha-equivalence axiomatisation. This gives
rise to a new notion of nominal unification, where solutions for unification problems are pairs of
a fixed-point context and a substitution. Although it may seem less natural than the standard
notion of nominal unifier based on freshness constraints, the notion of unifier based on fixedpoint
constraints behaves better when equational theories are considered: for example, nominal
unification remains finitary in the presence of commutativity, whereas it becomes infinitary when
unifiers are expressed using freshness contexts. | pt_BR |
| dc.description.unidade | Instituto de Ciências Exatas (IE) | - |
| dc.description.unidade | Departamento de Matemática (IE MAT) | - |
| Appears in Collections: | Trabalhos apresentados em evento
|
