Nesta tese apresentamos o projeto e a implementação do KEMS, um provador de teoremas multi-estratégia baseado no método de tablôs KE. Um provador de teoremas multi-estratégia é um provador de teoremas onde podemos variar as estratégias utilizadas sem modificar o núcleo da implementação. Além de multi-estratégia, o KEMS é capaz de provar teoremas em três sistemas lógicos: lógica clássica proposicional, mbC e mCi. Listamos abaixo algumas das contribuições deste trabalho: * um sistema KE para mbC que é analítico, correto e completo; * um sistema KE para mCi que é correto e completo; * um provador de teoremas multi-estratégia com as seguintes características: - aceita problemas em três sistemas lógicos: lógica clássica proposicional, mbC e mCi; - tem seis estratégias implementadas para lógica clássica proposicional, duas para mbC e duas para mCi; - tem treze ordenadores que são usados em conjunto com as estratégias; - implementa regras simplificadoras para lógica clássica proposicional; - possui uma interface gráfica que permite a visualização de provas; - é de código aberto e está disponível na Internet em http://kems.iv.fapesp.br; * benchmarks obtidos através da comparação das estratégias para lógica clássica proposicional resolvendo várias famílias de problemas; - sete famílias de problemas para avaliar provadores de teoremas paraconsistentes; * os primeiros benchmarks para as famílias de problemas para avaliar provadores de teoremas paraconsistentes. / In this thesis we present the design and implementation of KEMS, a multi-strategy theorem prover based on the KE tableau inference system. A multi-strategy theorem prover is a theorem prover where we can vary the strategy without modifying the core of the implementation. Besides being multi-strategy, KEMS is capable of proving theorems in three logical systems: classical propositional logic, mbC and mCi. We list below some of the contributions of this work: * an analytic, correct and complete KE system for mbC; * a correct and complete KE system for mCi; * a multi-strategy prover with the following characteristics: - accepts problems in three logical systems: classical propositional logic, mbC and mCi; - has 6 implemented strategies for classical propositional logic, 2 for mbC and 2 for mCi; - has 13 sorters to be used alongside with the strategies; - implements simplification rules of classical propositional logic; - provides a proof viewer with a graphical user interface; - it is open source and available on the internet at http://kems.iv.fapesp.br; * benchmark results obtained by KEMS comparing its classical propositional logic strategies with several problem families; * seven problem families designed to evaluate provers for logics of formal inconsistency; * the first benchmark results for the problem families designed to evaluate provers for logics of formal inconsistency.

Em Engenharia de Produção, os processos de decisão constituem um dos temas centrais e envolvem fatores de naturezas diversas, que os cercam de dificuldades. Nesses processos, não raramente, estão presentes fatores de natureza subjetiva, informações imprecisas, quando não vagas e mesmo conflitantes, que podem levar a decisões distorcidas, comprometendo a clareza e a objetividade de uma análise. Para manipular logicamente um conjunto de informações vagas, subjetivas, inconsistentes ou paracompletas, são necessárias lógicas alternativas da clássica, pois esta não pode, ao menos diretamente, ser empregada para tal fim. Assim, a lógica paraconsistente pode, em princípio, ser uma ferramenta adequada para a tarefa. No presente trabalho será apresentado um processo de auxílio às tomadas de decisão, denominado de Método de Análise pelo Baricentro (MAB), que se baseia na lógica paraconsistente anotada evidencial Et e no algoritmo para-analisador, introduzidos em (DA COSTA et al., 1999) e (DA SILVA FILHO; ABE, 2001). Esse método permite, de modo não trivial, o tratamento de informações com aquelas características e evidencia a possibilidade de aplicações da lógica Et em Administração, Marketing, Engenharia de Produção, previsão de diagnósticos, aplicações financeiras, entre outros temas. Um estudo de caso real, com resultados plenamente satisfatórios, mostra sua aplicabilidade na prática. Além disso, o MAB abre, entre outras, a perspectiva de se transformarem análises qualitativas em quantitativas. / In Production Engineering, decision making processes represent one of the most important topics and involve factors of various natures, which are, in turn, surrounded by difficulties. Quite often in these processes, there are factors of subjective nature, inaccurate data, sometimes even vague or conflicting information, which may lead to distorted decisions that eventually compromise the clarity and objectiveness of the analysis. In order to logically handle a set of vague, subjective, inconsistent or paracomplete information, logic other than classic is required, once the latter cannot, at least directly, be applied for such purpose. Hence, paraconsistent logic can, in principle, be an adequate tool for the task. In this paper, we will present an auxiliary process in decision making called Baricenter Analysis Method (BAM), which is based in Paraconsistent Annotated Evidential Logic Et and in a para-analyzer algorithm, introduced in (DA COSTA et al., 1999) and (DA SILVA FILHO; ABE, 2001). This methodology allows, in quite an unusual way, the treatment of information containing those characteristics and points out the possibility of applications of logic Et in Business Administration, Marketing, Production Engineering, anticipation of diagnosis, financial applications, among other subjects. Furthermore, BAM opens the possibility of transforming qualitative into quantitative analysis.

O Processamento e Análise Digital de Imagens é utilizado cada vez mais para agilizar processos, aumentar a precisão, segurança e confiabilidade de dados extraídos de imagens nas mais diversas áreas de pesquisa. No entanto, muitas vezes é necessário que o pesquisador faça, ele próprio, o pré-processamento das imagens, mesmo não sendo um especialista nesta área. Isto coloca em risco o próprio objetivo do uso do Processamento e Análise Digital de Imagens. Este trabalho analisa a relação dos dados extraídos de uma imagem (micrografia) através do software livre ImageJ com relação ao seu processamento final desejado, avaliando assim, a necessidade ou não, de uma ou mais sequencias de pré-processamento para adequar a imagem para o processamento final, indicando ainda quais fatores de influência apresentam informações irrelevantes ou incompletas para o processamento final utilizando ferramentas da Lógica Paraconsistente Anotada. Os resultados obtidos mostram que esta abordagem carece de informações diversificadas sobre a imagem original capturada que possam subsidiar a tomada de decisão quanto aos procedimentos necessários e, para o pré-processamento adequado ao objetivo desejado. / Processing and Analysis of Digital Images is increasingly used to streamline processes, improve accuracy, safety and reliability of data extracted from images in various research areas. However, it is often necessary for the researcher to make himself, the preprocessing of images, although not an expert in this area. This puts at risk the very purpose of using the Processing and Analysis of Digital Images. This paper analyzes the relationship of the data extracted from an image (micrograph) through the free software ImageJ, with respect to its desired final processing. Thus, evaluating the necessity or not, of one or more sequences of preprocessing to adjust the image to the final processing, further indicating which factors influence presents incomplete or irrelevant information for final processing using tools of Annotaded Paraconsistent Logic. The results show that this approach lacks diversified information about the original image captured that can support decision making about procedures for appropriate preprocessing to the desired goal.

Em Engenharia de Produção, os processos de decisão constituem um dos temas centrais e envolvem fatores de naturezas diversas, que os cercam de dificuldades. Nesses processos, não raramente, estão presentes fatores de natureza subjetiva, informações imprecisas, quando não vagas e mesmo conflitantes, que podem levar a decisões distorcidas, comprometendo a clareza e a objetividade de uma análise. Para manipular logicamente um conjunto de informações vagas, subjetivas, inconsistentes ou paracompletas, são necessárias lógicas alternativas da clássica, pois esta não pode, ao menos diretamente, ser empregada para tal fim. Assim, a lógica paraconsistente pode, em princípio, ser uma ferramenta adequada para a tarefa. No presente trabalho será apresentado um processo de auxílio às tomadas de decisão, denominado de Método de Análise pelo Baricentro (MAB), que se baseia na lógica paraconsistente anotada evidencial Et e no algoritmo para-analisador, introduzidos em (DA COSTA et al., 1999) e (DA SILVA FILHO; ABE, 2001). Esse método permite, de modo não trivial, o tratamento de informações com aquelas características e evidencia a possibilidade de aplicações da lógica Et em Administração, Marketing, Engenharia de Produção, previsão de diagnósticos, aplicações financeiras, entre outros temas. Um estudo de caso real, com resultados plenamente satisfatórios, mostra sua aplicabilidade na prática. Além disso, o MAB abre, entre outras, a perspectiva de se transformarem análises qualitativas em quantitativas. / In Production Engineering, decision making processes represent one of the most important topics and involve factors of various natures, which are, in turn, surrounded by difficulties. Quite often in these processes, there are factors of subjective nature, inaccurate data, sometimes even vague or conflicting information, which may lead to distorted decisions that eventually compromise the clarity and objectiveness of the analysis. In order to logically handle a set of vague, subjective, inconsistent or paracomplete information, logic other than classic is required, once the latter cannot, at least directly, be applied for such purpose. Hence, paraconsistent logic can, in principle, be an adequate tool for the task. In this paper, we will present an auxiliary process in decision making called Baricenter Analysis Method (BAM), which is based in Paraconsistent Annotated Evidential Logic Et and in a para-analyzer algorithm, introduced in (DA COSTA et al., 1999) and (DA SILVA FILHO; ABE, 2001). This methodology allows, in quite an unusual way, the treatment of information containing those characteristics and points out the possibility of applications of logic Et in Business Administration, Marketing, Production Engineering, anticipation of diagnosis, financial applications, among other subjects. Furthermore, BAM opens the possibility of transforming qualitative into quantitative analysis.

O Processamento e Análise Digital de Imagens é utilizado cada vez mais para agilizar processos, aumentar a precisão, segurança e confiabilidade de dados extraídos de imagens nas mais diversas áreas de pesquisa. No entanto, muitas vezes é necessário que o pesquisador faça, ele próprio, o pré-processamento das imagens, mesmo não sendo um especialista nesta área. Isto coloca em risco o próprio objetivo do uso do Processamento e Análise Digital de Imagens. Este trabalho analisa a relação dos dados extraídos de uma imagem (micrografia) através do software livre ImageJ com relação ao seu processamento final desejado, avaliando assim, a necessidade ou não, de uma ou mais sequencias de pré-processamento para adequar a imagem para o processamento final, indicando ainda quais fatores de influência apresentam informações irrelevantes ou incompletas para o processamento final utilizando ferramentas da Lógica Paraconsistente Anotada. Os resultados obtidos mostram que esta abordagem carece de informações diversificadas sobre a imagem original capturada que possam subsidiar a tomada de decisão quanto aos procedimentos necessários e, para o pré-processamento adequado ao objetivo desejado. / Processing and Analysis of Digital Images is increasingly used to streamline processes, improve accuracy, safety and reliability of data extracted from images in various research areas. However, it is often necessary for the researcher to make himself, the preprocessing of images, although not an expert in this area. This puts at risk the very purpose of using the Processing and Analysis of Digital Images. This paper analyzes the relationship of the data extracted from an image (micrograph) through the free software ImageJ, with respect to its desired final processing. Thus, evaluating the necessity or not, of one or more sequences of preprocessing to adjust the image to the final processing, further indicating which factors influence presents incomplete or irrelevant information for final processing using tools of Annotaded Paraconsistent Logic. The results show that this approach lacks diversified information about the original image captured that can support decision making about procedures for appropriate preprocessing to the desired goal.