Uma Análise dos Operadores de Revisão de Teorias do Sistema de Revisão FORTE_MBC
Autores
|
5625 |
2588,250
|
|
|
5626 |
2588,250
|
Informações:
Publicações do PESC
FORTE_MBC é um Sistema de Revisão de Teorias de Primeira-Ordem, construído a partir do FORTE mas com um importante complemento: ele usa a cláusula mais específica (Bottom Clause) e declaração de modos para definir o espaço de busca de literais. A introdução da Bottom Clause foi essencial para a redução do tempo de execução do processo de revisão (em média 55 vezes mais rápido), já que revisar teorias normalmente considera espaços de busca extensos, visto que refina teorias inteiras, ao invés de cláusulas individuais, uma por vez. Porém, a eficácia e a eficiência do processo de refinamento depende fortemente de outros fatores, como da ordem de generalidade que induz um modelo de generalização para o espaço de busca e, consequentemente, dos operadores de refinamento. Estes fatores nunca foram, até então, formalmente analisados no FORTE(_MBC). Nesta Tese contribuímos com (1) uma modificação dos modelos teóricos existentes para caracterizar operadores de refinamento, de forma a caracterizar o espaço de busca e os operadores de refinamento do FORTE_MBC; (2) uma melhoria nos operadores de refinamento de teorias do FORTE_MBC para torná-los ideais para o espaço definido. Por fim, a eficiência da revisão também é influenciada pelo total de átomos básicos vindos do Conhecimento Preliminar (BK). A Bottom Clause gerada no FORTE_MBC inclui todos os literais gerados a partir do BK que são relevantes para um exemplo dados certos parâmetros, podendo gerar espaços exponenciais. Porém, muitos destes literais não obedecem aos modos quando adicionados à cláusula sob revisão. Para amenizar este problema, propomos o sistema FORTE_BETH, que usa o algoritmo do sistema BETH para gerar uma Bottom Clause linear que contém apenas os literais que poderiam ser adicionados a uma cláusula de acordo com os modos definidos, o que tem o potencial de tornar o processo de revisão ainda mais eficiente.
FORTE_MBC is a First-Order Logic Theory Revision System, built upon FORTE but with an important supplement: it makes use of the Bottom Clause and modes declaration to define the search space of literals. Introducing the Bottom Clause was essential to reduce the runtime of the revision process (an average speed-up of 55), since revising theories usually considers large search spaces, mainly because it refines whole theories instead of stepwise individual clauses. However, the effectiveness and efficiency of the refinement process heavily relies on other factors, such as the generality relation that induces a generalization model for the search space, and, as a consequence, the refinement operators. These factors have never been formally analyzed in FORTE(_MBC) yet. In this work, we contribute with (1) a modification of the existing theoretical frameworks for characterizing refinement operators in order to characterize the search space and refinement operators of FORTE_MBC; (2) an improvement of the theory refinement operators of FORTE_MBC to make them ideal for the defined space. Finally, the efficiency of the review process is also influenced by the number of ground atoms from Background Knowledge (BK). The bottom clause generated in FORTE_MBC includes all literals created from BK that are relevant for some example, given some parameters, which can generate exponential spaces. However, many of those literals do not obey to the modes when are added to the clause under revision. To alleviate this problem, we propose the FORTE_BETH system, which use the BETH algorithm to generate a bottom clause of linear complexity that contains only the literals that could be included in a clause according to the modes defined, what can lead to a more efficient review process.