Tese (doutorado)—Universidade de Brasília, Instituto de Ciências Exatas, Departamento de Matemática, 2013. / Submitted by Letícia Gomes T. da Silva (leticiasilva@bce.unb.br) on 2013-11-27T16:07:18Z
No. of bitstreams: 1
2013_DanieleNantesSobrinho.pdf: 876137 bytes, checksum: 0a6a23afdf84d830cc314690803abe68 (MD5) / Approved for entry into archive by Guimaraes Jacqueline(jacqueline.guimaraes@bce.unb.br) on 2013-12-09T13:34:47Z (GMT) No. of bitstreams: 1
2013_DanieleNantesSobrinho.pdf: 876137 bytes, checksum: 0a6a23afdf84d830cc314690803abe68 (MD5) / Made available in DSpace on 2013-12-09T13:34:47Z (GMT). No. of bitstreams: 1
2013_DanieleNantesSobrinho.pdf: 876137 bytes, checksum: 0a6a23afdf84d830cc314690803abe68 (MD5) / Apresenta-se um algoritmo para decidir o problema da dedução do intruso (PDI) para a classe de teorias localmente estáveis normais, que incluem operadores associativos e comutativos (AC). A decidibilidade é baseada na análise de reduções de reescrita aplicadas na cabeça de termos que são construídos a partir de contextos normais e o conhecimento inicial de um intruso. Este algoritmo se baseia em um algoritmo eficiente para resolver um caso restrito de casamento módulo AC de ordem superior, obtido pela combinação de um algoritmo para Casamento AC com Ocorrências Distintas, e um algoritmo padrão para resolver sistemas de equações Diofantinas lineares. O algoritmo roda em tempo polinomial no tamanho de um conjunto saturado construído a partir do conhecimento inicial do intruso para a subclasse de teorias para a qual operadores AC possuem inversos. Os resultados são aplicados para teoria AC pura e a teoria de grupos Abelianos de ordem n dada. Uma tradução entre dedução natural e o cálculo de sequentes permite usar a mesma abordagem para decidir o problema da dedução elementar para teorias localmente estáveis com inversos. Como uma aplicação, a teoria de assinaturas cegas pode ser modelada e então, deriva-se um algoritmo para decidir o PDI neste contexto, estendendo resultados de decidibilidade prévios. ______________________________________________________________________________ ABSTRACT / We present an algorithm to decide the intruder deduction problem (IDP) for the class of normal locally stable theories, which include associative and commutative (AC) opera- tors. The decidability is based on the analysis of rewriting reductions applied in the head of terms built from normal contexts and the initial knowledge of the intruder. It relies on a new and efficient algorithm to solve a restricted case of higher-order AC-matching, obtained by combining the Distinct Occurrences of AC-matching algorithm and a stan- dard algorithm to solve systems of linear Diophantine equations. Our algorithm runs in polynomial time on the size of a saturation set built from the initial knowledge of the intruder for the subclass of theories for which AC operators have inverses. We apply the results to the Pure AC equational theory and Abelian Groups with a given order n. A translation between natural deduction and sequent calculus allows us to use the same approach to decide the elementary deduction problem for locally stable theories with inverses. As an application, we model the theory of blind signatures and derive an algorithm to decide IDP in this context, extending previous decidability results.
| Identifer | oai:union.ndltd.org:IBICT/oai:repositorio.unb.br:10482/14781 |
| Date | 06 September 2013 |
| Creators | Nantes Sobrinho, Daniele |
| Contributors | Fernández, Maribel, Ayala-Rincón, Mauricio |
| Source Sets | IBICT Brazilian ETDs |
| Language | Portuguese |
| Detected Language | English |
| Type | info:eu-repo/semantics/publishedVersion, info:eu-repo/semantics/doctoralThesis |
| Source | reponame:Repositório Institucional da UnB, instname:Universidade de Brasília, instacron:UNB |
| 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., info:eu-repo/semantics/openAccess |
Page generated in 0.0024 seconds