| Campo DC | Valor | Idioma |
|---|
| dc.contributor.advisor | Nalon, Cláudia | - |
| dc.contributor.author | Amaral, Lucas de Moura | - |
| dc.date.accessioned | 2019-10-22T22:09:29Z | - |
| dc.date.available | 2019-10-22T22:09:29Z | - |
| dc.date.issued | 2019-10-22 | - |
| dc.date.submitted | 2019-02-25 | - |
| dc.identifier.citation | AMARAL, Lucas de Moura. A resolution-based E-connected calculus. 2019. x, 61 f., il. Dissertação (Mestrado em Informática)—Universidade de Brasília, Brasília, 2019. | pt_BR |
| dc.identifier.uri | http://repositorio.unb.br/handle/10482/35640 | - |
| dc.description | Dissertação (mestrado)—Universidade de Brasília, Instituto de Ciências Exatas, Departamento de Ciência da Computação, 2019. | pt_BR |
| dc.description.abstract | Neste trabalho, apresentamos um cálculo para raciocinar sobre E-conexões, as quais
provêem um método computacionalmente robusto para combinar Abstract Description
Systems (ADSs) arbitrários. ADSs, introduzidos por Baader et al, são uma generalização
de várias lógicas, tais como temporais, espaciais, epistêmicas, lógicas descritivas e modais.
Provemos um cálculo baseado em resolução para lidar com conexões, assumindo que o
problema de satifatibilidade global das lógicas componentes é decidível. Isto nos permite
focar em raciocinar apenas sobre as restrições impostas pelas E-conexões, deixando o
raciocínio específico de cada domínio para as lógicas componentes.
Um dos passos mais importantes necessários para alcançar isto é a devida separação dos
elementos sintáticos relacionados às diferentes componentes, através de uma forma normal
proposta. Assim, provemos o conjunto completo de regras de transformação, apresentando
provas para a terminação e preservação de satisfatibilidade desta transformação.
Este trabalho apresenta as provas de correção, completude e terminação para o cálculo
proposto. Também disponibilizamos uma implementação prototípica, baseada no
provador KSP. Discutimos os resultados da avaliação e sugerimos algumas modificações
que podem ser feitas para melhorar a performance, abrindo caminho para o desenvolvimento
de uma futura implementação tanto modular quanto eficiente. | pt_BR |
| dc.description.sponsorship | Coordenação de Aperfeiçoamento de Pessoal de Nível Superior (CAPES). | pt_BR |
| dc.language.iso | Português | pt_BR |
| dc.rights | Acesso Aberto | pt_BR |
| dc.title | A resolution-based E-connected calculus | pt_BR |
| dc.type | Dissertação | pt_BR |
| dc.subject.keyword | Lógica modal | pt_BR |
| dc.subject.keyword | Raciocínio automático | pt_BR |
| dc.subject.keyword | E-conexões | pt_BR |
| dc.rights.license | 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. | pt_BR |
| dc.description.abstract1 | We introduce a calculus to reason about E-connections, which provide a computationally ro-
bust method to combine arbitrary Abstract Description Systems (ADSs). ADSs, introduced by
Baader et al, are a generalization of various logics such as temporal, spatial, epistemic descrip-
tion and modal logics in general. In this work, we restrict the logics to be combined to normal
modal logics. We provide a resolution-based calculus to deal with connections, assuming that
the global satisfiability problems of the component logics are decidable. This allows us to focus
on reasoning only about the restrictions imposed by the E-connections, leaving domain-specific
reasoning to the component logic.
One of the most important steps required to achieve this is the proper separation of syn-
tactical elements related to different components via a proposed normal form. Therefore, we
provide the full set of transformation rules, presenting proofs for termination and preservation
of satisfiability of this transformation.
This work presents the correctness, completeness and termination proofs for the proposed
calculus. We also make available a proof-of-concept implementation, based on the KSP prover.
We discuss the results of the evaluation and suggest some modifications that can be made to
improve performance, paving the way for the development of a future modular and efficient
implementation. | pt_BR |
| dc.description.unidade | Instituto de Ciências Exatas (IE) | pt_BR |
| dc.description.unidade | Departamento de Ciência da Computação (IE CIC) | pt_BR |
| dc.description.ppg | Programa de Pós-Graduação em Informática | pt_BR |
| Aparece nas coleções: | Teses, dissertações e produtos pós-doutorado
|
