Com o uso de um conceito ainda não explorado para fins de classificação de dados, baseado em Lógica Paraconsistente Anotada (LPA), este trabalho visa à construção de um sistema inteligente para classificação de gêneros musicais (Music Genre Classification - MGC). Este tema, de caráter emergente na literatura, tem recebido atenção crescente da comunidade científica, tendo em vista a sua grande aplicabilidade, destacando-se o potencial de comercialização de dados multimídia pela Internet, assim como a automatização de inúmeras tarefas de data mining que envolvem sinais musicais. Utilizando uma base de dados composta por amostras de músicas representativas de cada gênero musical, tais como jazz, bolero, bossa nova, forró, salsa e sertanejo, assim como de um classificador discriminativo paraconsistente, uma abordagem supervisionada é proposta para solucionar o problema. O primeiro módulo do sistema realiza a extração de características dos diversos segmentos das músicas com base na análise tempo-frequência associada com as bandas críticas do ouvido humano. Por outro lado, o segundo módulo utiliza o classificador proposto, que deve permitir a manipulação de sinais com características contraditórias de uma maneira mais semelhante àquela realizada pelo cérebro humano. Os resultados, quando comparados com as abordagens pré-existentes para MGC, demonstram a viabilidade do uso da LPA para tal fim. Além disso, caracteriza-se neste trabalho, uma contribuição original ao estado-da-arte no tema, que consiste justamente no uso da LPA para MGC, procedimento para o qual inexiste descrição na literatura até este momento. / By using a new concept, which is based on Paraconsistent Logic (LPA) and has not yet been applied for classification, this work aims at constructing an intelligent system for Music Genre Classification (MGC). This topic, that is emergent in the literature, has received an increasing attention from the scientific community due to its applicability, emphazising both a commercial potential to commercialize multimedia content on the Internet and data mining tasks involving music signals. By adopting a database formed by samples of songs, which represent different styles of music, such as jazz, bolero, bossa nova, forró, salsa and sertanejo, and a discriminative paraconsistent classifier, a supervised procedure is used to solve the problem. The system is divided in two modules. The first extracts features from the music files, based on the concepts of time-frequency analysis and crictical bands of the human ear. On the other hand, the second implements the proposed classifier, which allows an efficient treatment of contradictions in such a way that is more similar to the human brain. The results obtained, when compared with existing approaches used to MGC, demonstrate how LPA is suitable for this purpose. Additionally, this is the original contribution to the state-of-the-art: the use of LPA for MGC, an inexistent approach up to date.

Este trabalho desenvolve um modelo para análise de variáveis craniométricas que utiliza as Redes Neurais Artificiais Paraconsistentes, assentadas na Lógica Paraconsistente Anotada de dois valores. Tal lógica possui a capacidade de mensurar incerteza, inconsistência e paracompleteza. A Lógica Paraconsitente vem sendo empregada em diversas aplicações sujeitas a estas situações, constituindo nova ferramenta matemática em Inteligência Artificial. O trabalho tem como principal objetivo melhorar o diagnóstico cefalométrico. O modelo desenvolvido recebe as medidas das variáveis craniométricas de um determinado paciente e as compara com as médias das variáveis craniométricas normais de uma amostra da população brasileira. Esta amostra é composta de crianças e adolescentes de ambos os sexos, na faixa etária de 6 a 18 anos, utilizadas neste trabalho como valores de referência de normalidade. A análise cefalométrica aqui proposta consiste em quantificar discrepâncias esqueletais e dentárias sob a Lógica Paraconsistente. O uso das Redes Neurais Artificiais Paraconsistentes permite agregar ao méto do um fator de incerteza, respeitando o diagnóstico ortodôntico tradicional, e ao mesmo tempo, contextualiza diferentes regiões craniofaciais. O resultado da análise consiste dos graus de discrepância esqueletal, anteroposterior e vertical, e graus de discrepância dentárias, relativas aos incisivos inferiores e superiores. Variáveis craniométricas de 120 pacientes foram processadas pelo modelo proposto e avaliadas por três especialistas em Ortodontia. De acordo com o índice Kappa, houve desde concordância satisfatória até concordância quase perfeita entre o modelo e os especialistas, de acordo com as variáveis consideradas. As opiniões inter-especialista são substancialmente similares às comparações entre os especialistas e o modelo apresentado, o que reflete o potencial do modelo como um sistema especialista. A utilização de técnicas de Inteligência Artificial através da Lógica Paraconsistente, permitiu significante melhora na análise cefalométrica proposta. O modelo apresentado pode ser adaptado a outras amostras ou populações, com a adaptação dos valores de referência iniciais de normalidade. / This work shows the development of an unequal craniometric analysis model, which uses Paraconsistent Neural Network, based upon Paraconsistent Logic with two values. Such logical approach has the capability to handle concepts as uncertainness, inconsistency and paracompleteness. It has been used on diverse applications which present such features, constituting a new mathematical tool in Artificial Intelligence. The presented methodology had as main goal to booster diagnosis in Orthodontics. The developed model processes craniometric measures of a specific person, and compares to the expected means drawn from a Brazilian sample, comprised of children and adolescent individuals, ranging from 6 to 18 year-old, of both genders. The current cephalometric analysis, developed under the approach of Paraconsistent Logic, quantifies skeletal and dental discrepancies. The use of Paraconsistent Neural Network allows aggregating a factor of vagueness, respecting the limits of traditional orthodontic classification. At the same time, it contextualizes variables of different craniofacial regions. The results of the analysis are expressed through degrees of skeletal discrepancies, in the anteroposterior and vertical dimensions, and degrees of dental discrepancies, for the upper and lower incisors. Cephalometric va lues of a sample of 120 patients were processed by the paraconsistent model and analyzed by three specialists in Orthodontics. According to Kappa index, the agreement between the model and the specialists ranged from moderate to almost perfect, according to the variables considered. The inter-observer opinions were substantially similar to the mathematical model, which reflects the potential of the model as a specialist system. The use of Artificial Intelligence methods throughout Paraconsistent Logics, allowed significant improvement in cephalometric assessment. The presented model can be applied in different samples or populations, with adaptation of the degrees of normality as initial references.

Vários métodos estatísticos aplicados à medicina diagnóstica sofreram, nas últimas décadas, enormes avanços. Grande parte destes métodos está voltada ao problema de classificar indivíduos em grupos, sendo que os testes diagnósticos ligados a técnicas de Inteligência Artificial compõem nossa principal aplicação desse trabalho. Estes testes estatísticos são descritos como métodos teoricamente capazes de indicar a presença ou a ausência de uma determinada doença, com certa chance de erro. A quantificação destas chances de erro que é, basicamente, o objetivo destes métodos tem servido a inúmeras aplicações e nesse trabalho é utilizada como fonte de evidências para os procedimentos de análises estruturados em Lógica Paraconsistente. Como a Lógica Paraconsistente é uma lógica não-clássica que aceita contradição em sua estrutura sem invalidar as conclusões, e utiliza em suas análises valores evidenciais, aplicamos aqui os conceitos fundamentais de um tipo de Lógica Paraconsistente denominada de Lógica Paraconsistente Anotada com anotação de dois valores LPA2v. Através dos procedimentos estatísticos e os fundamentos da LPA2v o presente estudo objetiva descrever a situação em que o teste produz uma resposta que não é descrita simplesmente como positivo ou negativo, mas por um resultado que pode ser expresso por uma variável categórica ordinal ou por uma variável contínua que pode ser considerada como grau de evidência. Esse processo é realizado utilizando uma dedução lógica que usa os conceitos da Probabilidade Pragmática na qual se pode efetuar uma ligação entre a teoria probabilística de Bayes e os métodos de aplicação da Lógica Paraconsistente Anotada com dois valores LPA2v. Dessa junção surgiram neste trabalho algoritmos Paraconsistentes que descrevem esse processo. Denominamos o processo de adaptação da Teoria de Bayes para a Lógica Paraconsistente de ParaBayes. Para demonstrar os procedimentos que utilizam os conceitos fundamentais da LPA2v em dados probabilísticos foram extraídos valores evidenciais de um banco de dados que se refere à submissão de um conjunto de casos, contendo uma série de evidências e o diagnóstico de Diabetes, em uma comunidade de índias PIMA. São utilizadas no banco de dados índias PIMA as técnicas dos métodos estatísticos e de raciocínio probabilístico de Bayes para levantamento de dados que foram interpretados e modelados como Graus de Evidência capazes de serem analisados pelos Algoritmos da LPA2v. Neste estudo verifica-se que a extração dos Graus de Evidência não invalida as técnicas estatísticas já estabelecidas, mas confere através da LPA2v novas formas de interpretação baseadas nos resultados e produzindo meios que facilitam o tratamento dos dados por ferramentas computacionais elevando o grau de confiança dos diagnósticos. Uma das observações importantes é que o método LPA2v/Bayes proposto utilizado para extrair evidências é capaz de evitar possíveis distorções no formato da curva que possam advir da seleção inadequada de casos de teste. Os resultados obtidos sugerem que em situações nas quais se tenha uma grande quantidade de casos em que as incertezas exijam métodos estatísticos para formar diagnóstico, esta seja uma boa técnica para se adotar em sistemas de apoio a decisão médica. / Several statistical methods applied to the medicine diagnostic suffered, in the last decades, enormous progresses. Great part of these methods come back to the problem from classifying individuals in groups. Tests that use techniques of Artificial Intelligence compose our main main focus. Statistical tests are described as methods capable to indicate the presence or the absence of a certain disease, with a certain chance of error. The quantification of these error chances that is, basically, the objective of these methods has served to countless applications. In this work it is used as source of evidence for the procedures of analysis structured through Paraconsistent Logic. As Paraconsistent Logic is a non-classic logic that accepts contradiction in its structure without invalidating the conclusions and uses in its analysis values attributed to evidences, we applied the fundamental concepts of a type of Logic denominated Paraconsistent Logic Annotated with two values LPA2v. Through the statistical procedures and the foundations of LPA2v the present study aims at describing the situation where the test produces an answer that is not simply described as \"positive\" or \"negative\", but can be expressed by an ordinal variable or by a continuous variable that can be considered as an evidence degree. That process is obtained using a logical deduction that uses the concepts of the Pragmatic Probability where it can make a connection between the probabilistic theory of Bayes and the methods of Paraconsistent Logic, Annotated with two values, LPA2v. Out of that junction Paraconsistent algorithms appeared in this work that describe the whole process. We denominated the process of adaptation of the Theory of Bayes to Paraconsistent Logic of ParaBayes. To demonstrate the procedures that use the fundamental concepts of LPA2v evidence values were extracted from a database comprising a series of evidences and the diagnosis of Diabetes, in a community of PIMA Indians. The PIMA Indian database was a test-bed field for the techniques of the statistical methods and of reasoning probabilistic of Bayes for rising of data that were interpreted and modeled as Degrees of Evidence capable of being analyzed by the Algorithms of LPA2v. In this study it is verified that the extraction of the Degrees of Evidence doesn\'t invalidate the statistical techniques established, but it allows for new forms of interpretations based on the results and producing means that facilitate the treatment of the data, elevating the trust in the diagnostic. One of the important observations is that the proposed method LPA2v/Bayes used to extract evidence is capable to avoid possible distortions in the format of the curve that is usually the result of inadequate selection of test cases. Results suggest that in situations where a great amount of cases have uncertainties this is a good technique to adopt in medical decision support systems.

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.

Vários métodos estatísticos aplicados à medicina diagnóstica sofreram, nas últimas décadas, enormes avanços. Grande parte destes métodos está voltada ao problema de classificar indivíduos em grupos, sendo que os testes diagnósticos ligados a técnicas de Inteligência Artificial compõem nossa principal aplicação desse trabalho. Estes testes estatísticos são descritos como métodos teoricamente capazes de indicar a presença ou a ausência de uma determinada doença, com certa chance de erro. A quantificação destas chances de erro que é, basicamente, o objetivo destes métodos tem servido a inúmeras aplicações e nesse trabalho é utilizada como fonte de evidências para os procedimentos de análises estruturados em Lógica Paraconsistente. Como a Lógica Paraconsistente é uma lógica não-clássica que aceita contradição em sua estrutura sem invalidar as conclusões, e utiliza em suas análises valores evidenciais, aplicamos aqui os conceitos fundamentais de um tipo de Lógica Paraconsistente denominada de Lógica Paraconsistente Anotada com anotação de dois valores LPA2v. Através dos procedimentos estatísticos e os fundamentos da LPA2v o presente estudo objetiva descrever a situação em que o teste produz uma resposta que não é descrita simplesmente como positivo ou negativo, mas por um resultado que pode ser expresso por uma variável categórica ordinal ou por uma variável contínua que pode ser considerada como grau de evidência. Esse processo é realizado utilizando uma dedução lógica que usa os conceitos da Probabilidade Pragmática na qual se pode efetuar uma ligação entre a teoria probabilística de Bayes e os métodos de aplicação da Lógica Paraconsistente Anotada com dois valores LPA2v. Dessa junção surgiram neste trabalho algoritmos Paraconsistentes que descrevem esse processo. Denominamos o processo de adaptação da Teoria de Bayes para a Lógica Paraconsistente de ParaBayes. Para demonstrar os procedimentos que utilizam os conceitos fundamentais da LPA2v em dados probabilísticos foram extraídos valores evidenciais de um banco de dados que se refere à submissão de um conjunto de casos, contendo uma série de evidências e o diagnóstico de Diabetes, em uma comunidade de índias PIMA. São utilizadas no banco de dados índias PIMA as técnicas dos métodos estatísticos e de raciocínio probabilístico de Bayes para levantamento de dados que foram interpretados e modelados como Graus de Evidência capazes de serem analisados pelos Algoritmos da LPA2v. Neste estudo verifica-se que a extração dos Graus de Evidência não invalida as técnicas estatísticas já estabelecidas, mas confere através da LPA2v novas formas de interpretação baseadas nos resultados e produzindo meios que facilitam o tratamento dos dados por ferramentas computacionais elevando o grau de confiança dos diagnósticos. Uma das observações importantes é que o método LPA2v/Bayes proposto utilizado para extrair evidências é capaz de evitar possíveis distorções no formato da curva que possam advir da seleção inadequada de casos de teste. Os resultados obtidos sugerem que em situações nas quais se tenha uma grande quantidade de casos em que as incertezas exijam métodos estatísticos para formar diagnóstico, esta seja uma boa técnica para se adotar em sistemas de apoio a decisão médica. / Several statistical methods applied to the medicine diagnostic suffered, in the last decades, enormous progresses. Great part of these methods come back to the problem from classifying individuals in groups. Tests that use techniques of Artificial Intelligence compose our main main focus. Statistical tests are described as methods capable to indicate the presence or the absence of a certain disease, with a certain chance of error. The quantification of these error chances that is, basically, the objective of these methods has served to countless applications. In this work it is used as source of evidence for the procedures of analysis structured through Paraconsistent Logic. As Paraconsistent Logic is a non-classic logic that accepts contradiction in its structure without invalidating the conclusions and uses in its analysis values attributed to evidences, we applied the fundamental concepts of a type of Logic denominated Paraconsistent Logic Annotated with two values LPA2v. Through the statistical procedures and the foundations of LPA2v the present study aims at describing the situation where the test produces an answer that is not simply described as \"positive\" or \"negative\", but can be expressed by an ordinal variable or by a continuous variable that can be considered as an evidence degree. That process is obtained using a logical deduction that uses the concepts of the Pragmatic Probability where it can make a connection between the probabilistic theory of Bayes and the methods of Paraconsistent Logic, Annotated with two values, LPA2v. Out of that junction Paraconsistent algorithms appeared in this work that describe the whole process. We denominated the process of adaptation of the Theory of Bayes to Paraconsistent Logic of ParaBayes. To demonstrate the procedures that use the fundamental concepts of LPA2v evidence values were extracted from a database comprising a series of evidences and the diagnosis of Diabetes, in a community of PIMA Indians. The PIMA Indian database was a test-bed field for the techniques of the statistical methods and of reasoning probabilistic of Bayes for rising of data that were interpreted and modeled as Degrees of Evidence capable of being analyzed by the Algorithms of LPA2v. In this study it is verified that the extraction of the Degrees of Evidence doesn\'t invalidate the statistical techniques established, but it allows for new forms of interpretations based on the results and producing means that facilitate the treatment of the data, elevating the trust in the diagnostic. One of the important observations is that the proposed method LPA2v/Bayes used to extract evidence is capable to avoid possible distortions in the format of the curve that is usually the result of inadequate selection of test cases. Results suggest that in situations where a great amount of cases have uncertainties this is a good technique to adopt in medical decision support systems.

Com o uso de um conceito ainda não explorado para fins de classificação de dados, baseado em Lógica Paraconsistente Anotada (LPA), este trabalho visa à construção de um sistema inteligente para classificação de gêneros musicais (Music Genre Classification - MGC). Este tema, de caráter emergente na literatura, tem recebido atenção crescente da comunidade científica, tendo em vista a sua grande aplicabilidade, destacando-se o potencial de comercialização de dados multimídia pela Internet, assim como a automatização de inúmeras tarefas de data mining que envolvem sinais musicais. Utilizando uma base de dados composta por amostras de músicas representativas de cada gênero musical, tais como jazz, bolero, bossa nova, forró, salsa e sertanejo, assim como de um classificador discriminativo paraconsistente, uma abordagem supervisionada é proposta para solucionar o problema. O primeiro módulo do sistema realiza a extração de características dos diversos segmentos das músicas com base na análise tempo-frequência associada com as bandas críticas do ouvido humano. Por outro lado, o segundo módulo utiliza o classificador proposto, que deve permitir a manipulação de sinais com características contraditórias de uma maneira mais semelhante àquela realizada pelo cérebro humano. Os resultados, quando comparados com as abordagens pré-existentes para MGC, demonstram a viabilidade do uso da LPA para tal fim. Além disso, caracteriza-se neste trabalho, uma contribuição original ao estado-da-arte no tema, que consiste justamente no uso da LPA para MGC, procedimento para o qual inexiste descrição na literatura até este momento. / By using a new concept, which is based on Paraconsistent Logic (LPA) and has not yet been applied for classification, this work aims at constructing an intelligent system for Music Genre Classification (MGC). This topic, that is emergent in the literature, has received an increasing attention from the scientific community due to its applicability, emphazising both a commercial potential to commercialize multimedia content on the Internet and data mining tasks involving music signals. By adopting a database formed by samples of songs, which represent different styles of music, such as jazz, bolero, bossa nova, forró, salsa and sertanejo, and a discriminative paraconsistent classifier, a supervised procedure is used to solve the problem. The system is divided in two modules. The first extracts features from the music files, based on the concepts of time-frequency analysis and crictical bands of the human ear. On the other hand, the second implements the proposed classifier, which allows an efficient treatment of contradictions in such a way that is more similar to the human brain. The results obtained, when compared with existing approaches used to MGC, demonstrate how LPA is suitable for this purpose. Additionally, this is the original contribution to the state-of-the-art: the use of LPA for MGC, an inexistent approach up to date.

This thesis studies the extensions of the four-valued Belnap-Dunn logic, called super-Belnap logics, from the point of view of abstract algebraic logic. We describe the global structure of the lattice of super-Belnap logics and show that this lattice can be fully described in terms of classes of finite graphs satisfying some closure conditions. We also introduce a theory of so- called explosive extensions and use it to prove new completeness theorems for super-Belnap logics. A Gentzen-style proof theory for these logics is then developed and used to establish interpolation for many of them. Finally, we also study the expansion of the Belnap-Dunn logic by the truth operator ∆. Keywords: abstract algebraic logic, Belnap-Dunn logic, paraconsistent logic, super-Belnap logics

Este trabalho desenvolve um modelo para análise de variáveis craniométricas que utiliza as Redes Neurais Artificiais Paraconsistentes, assentadas na Lógica Paraconsistente Anotada de dois valores. Tal lógica possui a capacidade de mensurar incerteza, inconsistência e paracompleteza. A Lógica Paraconsitente vem sendo empregada em diversas aplicações sujeitas a estas situações, constituindo nova ferramenta matemática em Inteligência Artificial. O trabalho tem como principal objetivo melhorar o diagnóstico cefalométrico. O modelo desenvolvido recebe as medidas das variáveis craniométricas de um determinado paciente e as compara com as médias das variáveis craniométricas normais de uma amostra da população brasileira. Esta amostra é composta de crianças e adolescentes de ambos os sexos, na faixa etária de 6 a 18 anos, utilizadas neste trabalho como valores de referência de normalidade. A análise cefalométrica aqui proposta consiste em quantificar discrepâncias esqueletais e dentárias sob a Lógica Paraconsistente. O uso das Redes Neurais Artificiais Paraconsistentes permite agregar ao méto do um fator de incerteza, respeitando o diagnóstico ortodôntico tradicional, e ao mesmo tempo, contextualiza diferentes regiões craniofaciais. O resultado da análise consiste dos graus de discrepância esqueletal, anteroposterior e vertical, e graus de discrepância dentárias, relativas aos incisivos inferiores e superiores. Variáveis craniométricas de 120 pacientes foram processadas pelo modelo proposto e avaliadas por três especialistas em Ortodontia. De acordo com o índice Kappa, houve desde concordância satisfatória até concordância quase perfeita entre o modelo e os especialistas, de acordo com as variáveis consideradas. As opiniões inter-especialista são substancialmente similares às comparações entre os especialistas e o modelo apresentado, o que reflete o potencial do modelo como um sistema especialista. A utilização de técnicas de Inteligência Artificial através da Lógica Paraconsistente, permitiu significante melhora na análise cefalométrica proposta. O modelo apresentado pode ser adaptado a outras amostras ou populações, com a adaptação dos valores de referência iniciais de normalidade. / This work shows the development of an unequal craniometric analysis model, which uses Paraconsistent Neural Network, based upon Paraconsistent Logic with two values. Such logical approach has the capability to handle concepts as uncertainness, inconsistency and paracompleteness. It has been used on diverse applications which present such features, constituting a new mathematical tool in Artificial Intelligence. The presented methodology had as main goal to booster diagnosis in Orthodontics. The developed model processes craniometric measures of a specific person, and compares to the expected means drawn from a Brazilian sample, comprised of children and adolescent individuals, ranging from 6 to 18 year-old, of both genders. The current cephalometric analysis, developed under the approach of Paraconsistent Logic, quantifies skeletal and dental discrepancies. The use of Paraconsistent Neural Network allows aggregating a factor of vagueness, respecting the limits of traditional orthodontic classification. At the same time, it contextualizes variables of different craniofacial regions. The results of the analysis are expressed through degrees of skeletal discrepancies, in the anteroposterior and vertical dimensions, and degrees of dental discrepancies, for the upper and lower incisors. Cephalometric va lues of a sample of 120 patients were processed by the paraconsistent model and analyzed by three specialists in Orthodontics. According to Kappa index, the agreement between the model and the specialists ranged from moderate to almost perfect, according to the variables considered. The inter-observer opinions were substantially similar to the mathematical model, which reflects the potential of the model as a specialist system. The use of Artificial Intelligence methods throughout Paraconsistent Logics, allowed significant improvement in cephalometric assessment. The presented model can be applied in different samples or populations, with adaptation of the degrees of normality as initial references.

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.