Made available in DSpace on 2014-12-17T15:12:12Z (GMT). No. of bitstreams: 1 DavidGC_DISSERT.pdf: 766947 bytes, checksum: f1a6301612dd36741701f971f1734291 (MD5) Previous issue date: 2010-01-15 / Formalization of logical systems in natural deduction brings many metatheoretical advantages, which Normalization proof is always highlighted. Modal logic systems, until very recently, were not routinely formalized in natural deduction, though some formulations and Normalization proofs are known. This work is a presentation of some important known systems of modal logic in natural deduction, and some Normalization procedures for them, but it is also and mainly a presentation of a hierarchy of modal logic systems in natural deduction, from K until S5, together with an outline of a Normalization proof for the system K, which is a model for Normalization in other systems / A formaliza??o de sistemas de l?gica em dedu??o natural traz muitas vantagens meta-teor?ticas, das quais ? sempre destacada a prova de normaliza??o. Os sistemas de l?gica modal at? bem recentemente n?o eram costumeiramente tratados pelo vi?s da dedu??o natural, contudo algumas formula??es, provas de normaliza??o e tentativas de provas surgiram. Esse trabalho ? uma apresenta??o de alguns sistemas importantes de l?gica modal em dedu??o natural j? existentes, e de alguns procedimentos de normaliza??o para eles, mas ? tamb?m, e principalmente, a apresenta??o de uma hierarquia de sistemas de l?gica modal em Dedu??o Natural do sistema K ao sistema S5 e um esquema da prova de normaliza??o do sistema K, que ? modelo para a normaliza??o nos outros sistemas

Made available in DSpace on 2015-03-03T15:47:48Z (GMT). No. of bitstreams: 1 AdrianoAD_DISSERT.pdf: 771338 bytes, checksum: 06adea5feab9914c5a48eb146511b556 (MD5) Previous issue date: 2013-11-19 / Coordena??o de Aperfei?oamento de Pessoal de N?vel Superior / I thank to my advisor, Jo?o Marcos, for the intellectual support and patience that devoted me along graduate years. With his friendship, his ability to see problems of the better point of view and his love in to make Logic, he became a great inspiration for me. I thank to my committee members: Claudia Nalon, Elaine Pimentel and Benjamin Bedregal. These make a rigorous lecture of my work and give me valuable suggestions to make it better. I am grateful to the Post-Graduate Program in Systems and Computation that accepted me as student and provided to me the propitious environment to develop my research. I thank also to the CAPES for a 21 months fellowship. Thanks to my research group, LoLITA (Logic, Language, Information, Theory and Applications). In this group I have the opportunity to make some friends. Someone of them I knew in my early classes, they are: Sanderson, Haniel and Carol Blasio. Others I knew during the course, among them I?d like to cite: Patrick, Claudio, Flaulles and Ronildo. I thank to Severino Linhares and Maria Linhares who gently hosted me at your home in my first months in Natal. This couple jointly with my colleagues of student flat Fernado, Don?tila and Aline are my nuclear family in Natal. I thank my fianc?e Lucl?cia for her precious a ective support and to understand my absence at home during my master. I thank also my parents Manoel and Zenilda, my siblings Alexandre, Paulo and Paula.Without their confidence and encouragement I wouldn?t achieve success in this journey. If you want the hits, be prepared for the misses Carl Yastrzemski / Esta disserta??o trata do enriquecimento de l?gicas modais. O termo enriquecimento ? usado em dois sentidos distintos. No primeiro deles, de fundo sem?ntico, propomos uma sem?ntica difusa para diversas l?gicas modais normais e demonstramos um resultado de completude para uma extensa classe dessas l?gicas enriquecidas com m?ltiplas inst?ncias do axioma da conflu?ncia. Um fato curioso a respeito dessa sem?ntica ? que ela se comporta como as sem?nticas de Kripke usuais. O outro enriquecimento diz respeito ? expressividade da l?gica e se d? por meio da adi??o de novos conectivos, especialmente de nega??es modais. Neste sentido, estudamos inicialmente o fragmento da l?gica cl?ssica positiva estendido com uma nega??o modal paraconsistente e mostramos que essa linguagem ? forte o suficiente para expressar as linguagens modais normais. Vemos que tamb?m ? poss?vel definir uma nega??o modal paracompleta e conectivos de restaura??o que internalizam as no??es de consist?ncia e determina??o a n?vel da linguagem-objeto. Esta l?gica constitui-se em uma L?gica da Inconsist?ncia Formal e em uma L?gica da Indetermina??o Formal. Em tais l?gicas, com o objetivo de recuperar infer?ncias cl?ssicas perdidas, demonstram-se Teoremas de Ajuste de Derivabilidade. No caso da l?gica estendida com uma nega??o paraconsistente, se removermos a implica??o ainda lidaremos com uma linguagem bastante rica, com ambas nega??es paranormais e seus respectivos conectivos de restaura??o. Sobre esta linguagem estudamos a l?gica modal normal minimal definida por meio de um c?lculo de Gentzen apropriado, ? diferen?a dos demais sistemas estudados at? ent?o, que s?o apresentados via c?lculo de Hilbert. Em seguida ap?s demonstrarmos a completude do sistema dedutivo associado a este c?lculo, introduzimos algumas extens?es desse sistema e buscamos Teoremas de Ajuste de Derivabilidade adequados

Submitted by Automa??o e Estat?stica (sst@bczm.ufrn.br) on 2017-04-03T22:46:24Z No. of bitstreams: 1 LauraFernandesDellOrto_DISSERT.pdf: 866111 bytes, checksum: 0ef11e74d1508214463b993885352d6c (MD5) / Approved for entry into archive by Arlan Eloi Leite Silva (eloihistoriador@yahoo.com.br) on 2017-04-11T20:56:41Z (GMT) No. of bitstreams: 1 LauraFernandesDellOrto_DISSERT.pdf: 866111 bytes, checksum: 0ef11e74d1508214463b993885352d6c (MD5) / Made available in DSpace on 2017-04-11T20:56:41Z (GMT). No. of bitstreams: 1 LauraFernandesDellOrto_DISSERT.pdf: 866111 bytes, checksum: 0ef11e74d1508214463b993885352d6c (MD5) Previous issue date: 2017-02-15 / Em L?gica Cl?ssica, podemos utilizar as hip?teses um n?mero indeterminado de vezes. Por exemplo, a prova de um teorema pode fazer uso do mesmo lema v?rias vezes. Por?m, em sistemas f?sicos, qu?micos e computacionais a situa??o ? diferente: um recurso n?o pode ser reutilizado ap?s ser consumido em uma a??o. Em L?gica Linear, f?rmulas s?o vistas como recursos a serem utilizados durante a prova. ? essa no??o de recursos que faz a L?gica Linear ser interessante para a modelagem de sistemas. Para tanto, a L?gica Linear controla o uso da contra??o e do enfraquecimento atrav?s dos exponenciais ! e ?. Este trabalho tem como objetivo fazer um estudo sobre a L?gica Linear com Subexponenciais (SELL), que ? um refinamento da L?gica Linear. Em SELL, os exponenciais da L?gica Linear possuem ?ndices, isto ?, ! e ? ser?o substitu?dos por !i e ?i, onde ?i? ? um ?ndice. Um dos pontos fundamentais de Teoria da Prova ? a prova da Elimina??o do Corte, que neste trabalho ? demonstrada tanto para L?gica Linear como para SELL, onde apresentamos detalhes que normalmente s?o omitidos. A partir do teorema de Elimina??o do Corte, podemos concluir a consist?ncia do sistema (para as l?gicas que estamos utilizando) e outros resultados como a propriedade de subf?rmula. O trabalho inicia-se com um cap?tulo de Teoria da Prova, e em seguida se faz uma exposi??o sobre a L?gica Linear. Assim, com essas bases, apresenta-se a L?gica Linear com Subexponenciais. SELL tem sido utilizada, por exemplo, na especifica??o e verifica??o de diferentes sistemas tais como sistemas bioqu?micos, sistemas de intera??o multim?dia e, em geral, em sistemas concorrentes com modalidades temporais, espaciais e epist?micas. Com essa base te?rica bastante clara, apresenta-se a especifica??o de um sistema bioqu?mico utilizando SELL. Al?m disso, apresentamos v?rias inst?ncias de SELL que tem interpreta??es interessantes do ponto de vista computacional. / In Classical Logic, we can use a given hypothesis an indefinite number of times. For example, the proof of a theorem may use the same lemma several times. However, in physical, chemical and computational systems, the situation is different: a resource cannot be reused after being consumed in one action. In Linear Logic, formulas are seen as resources to be used during a proof. This feature makes Linear Logic an interesting formalism for the specification and verification of such systems. Linear Logic controls the rules of contraction and weakening through the exponentials ! and ?. This work aims to study Linear Logic with subexponentials (SELL), which is a refinement of Linear Logic. In SELL, the exponentials of Linear Logic are decorated with indexes, i.e., ! and ? are replaced with !i and ?i, where ?i? is an index. One of the main results in Proof Theory is the Cut-Elimination theorem. In this work we demonstrate that theorem for both Linear Logic and SELL, where we present details that are usually omitted in the literature. From the Cut-Elimination Theorem, we can show, as a corollary, the consistency of the system (for the logics considered here) and other results as the subformula property. This work begins with an introduction to Proof Theory and then, it presents Linear Logic. On these bases, we present Linear Logic with subexponentials. SELL has been used, for example, in the specification and verification of various systems such as biochemical systems, multimedia interaction systems and, in general, concurrent systems with temporal, spatial and epistemic modalities. Using the theory of SELL, we show the specification of a biochemical system. Moreover, we present several instances of SELL that have interesting interpretations from a computational point of view.

Made available in DSpace on 2014-12-17T15:12:11Z (GMT). No. of bitstreams: 1 AdrianoMS_DISSERT.pdf: 2088118 bytes, checksum: dd824a46d35773271668ba84f8280fa8 (MD5) Previous issue date: 2009-12-15 / The main goal of this work is to clarify the central concepts involved in the study of formalization of conditional sentences. More specifically, it has been done a comparative analysis of the two greater and more traditional proposals of conditional formalization (Lewis 1973c e Adams 1975). These proposals were responsible for the creation of a way of analysis that still present in the current debate about this subject. This work pursues to explain the principal assumptions held within these proposals. According to certain disambiguation techniques from Bennett (2003) and Lycan (2005), this work tries to explicit how these assumptions connect to the aims sought by the initial approaches. The following results show that there is a not declared presumption, the definition of the object of study of these theories, i.e., the definition of conditional sentence. This work argues that despite of not explicitly declared the definition of the study object has a central role in the intelligibility of the debate itself / estudo da formaliza??o das senten?as condicionais. Mais especificamente, empreendemos uma an?lise comparativa de duas das principais e mais tradicionais propostas de formaliza??o dos condicionais (Lewis (1973c) e Adams (1975)), propostas respons?veis pela inaugura??o de vertentes de an?lise que ainda se fazem presentes no debate contempor?neo sobre o tema. Visamos, fundamentalmente, o esclarecimento das principais assun??es presentes nessas propostas. Com base em certas t?cnicas de desambigua??o presentes em Bennett (2003) e em Lycan (2005), buscamos explicitar como essas assun??es articulam-se, efetivamente, aos objetivos almejados pelas abordagens inaugurais. Os resultados que se seguem mostram que existe um pressuposto, n?o explicitamente declarado, t?cito, a defini??o do objeto de estudo dessas teorias, isto ?, a defini??o de senten?a condicional. Argumentamos que, apesar de n?o claramente declarada, a defini??o do objeto de estudo desempenha um papel fundamental na pr?pria inteligibilidade do debate

Submitted by Automa??o e Estat?stica (sst@bczm.ufrn.br) on 2017-02-02T14:41:50Z No. of bitstreams: 1 JeffersonAlexandreDoNascimento_DISSERT.pdf: 6450548 bytes, checksum: 492fdc86c5c402671b6257d90803e044 (MD5) / Approved for entry into archive by Arlan Eloi Leite Silva (eloihistoriador@yahoo.com.br) on 2017-02-09T17:30:36Z (GMT) No. of bitstreams: 1 JeffersonAlexandreDoNascimento_DISSERT.pdf: 6450548 bytes, checksum: 492fdc86c5c402671b6257d90803e044 (MD5) / Made available in DSpace on 2017-02-09T17:30:36Z (GMT). No. of bitstreams: 1 JeffersonAlexandreDoNascimento_DISSERT.pdf: 6450548 bytes, checksum: 492fdc86c5c402671b6257d90803e044 (MD5) Previous issue date: 2016-08-09 / A presente disserta??o tem por objetivo principal, apresentar uma proposta de ensino da l?gica matem?tica no ?mbito do Ensino M?dio, elencando fatores que baseados nos principais documentos oficiais que regem a educa??o no Brasil, mostram a import?ncia da inser??o da l?gica na grade curricular do Ensino M?dio. O trabalho est? dividido em 4 partes, nas quais est?o apresentadas a hist?ria da l?gica proposicional, a teoria, aplica??es da l?gica nas demonstra??es matem?ticas e atividades propostas ? serem aplicadas em sala de aula. / This work has as main objective to present a proposal for logic teaching mathematics in the high school, listing factors based on key documents official governing education in Brazil, show the importance of logic integration in curriculumof high school . The work is divided into 4 parts, which are presented in the history of propositional logic, theory, logic applications in mathematical demonstrations and activities proposed to They are applied in the classroom.

Submitted by Automa??o e Estat?stica (sst@bczm.ufrn.br) on 2018-03-02T23:39:14Z No. of bitstreams: 1 ThiagoNascimentoDaSilva_DISSERT.pdf: 675458 bytes, checksum: 9123812e69a846020d3cd6346e530e1e (MD5) / Approved for entry into archive by Arlan Eloi Leite Silva (eloihistoriador@yahoo.com.br) on 2018-03-13T18:55:45Z (GMT) No. of bitstreams: 1 ThiagoNascimentoDaSilva_DISSERT.pdf: 675458 bytes, checksum: 9123812e69a846020d3cd6346e530e1e (MD5) / Made available in DSpace on 2018-03-13T18:55:45Z (GMT). No. of bitstreams: 1 ThiagoNascimentoDaSilva_DISSERT.pdf: 675458 bytes, checksum: 9123812e69a846020d3cd6346e530e1e (MD5) Previous issue date: 2018-01-25 / Al?m da mais conhecida l?gica de Nelson (?3) e da l?gica paraconsistente de Nelson (?4), David Nelson introduziu no artigo de 1959 "Negation and separation of concepts in constructive systems", com motiva??es de aritm?tica e construtividade, a l?gica que ele chamou de "?". Naquele trabalho, a l?gica ? definida por meio de um c?lculo (que carece crucialmente da regra de contra??o) tendo infinitos esquemas de regras, e nenhuma sem?ntica ? fornecida. Neste trabalho n?s tomamos o fragmento proposicional de ?, mostrando que ele ? algebriz?vel (de fato, implicativo) no sentido de Blok & Pigozzi com respeito a uma classe de reticulados residuados involutivos. Assim, fornecemos a primeira sem?ntica para ? (que chamamos de ?-?lgebras), bem como um c?lculo estilo Hilbert finito equivalente ? apresenta??o de Nelson. Fornecemos um algoritmo para construir ?-?lgebras a partir de ?-?lgebras ou reticulados implicativos e demonstramos alguns resultados sobre a classe de ?lgebras que introduzimos. N?s tamb?m comparamos ? com outras l?gicas da fam?lia de Nelson, a saber, ?3 e ?4. / Besides the better-known Nelson logic (?3) and paraconsistent Nelson logic (?4), in Negation and separation of concepts in constructive systems (1959) David Nelson introduced a logic that he called ?, with motivations of arithmetic and constructibility. The logic was defined by means of a calculus (crucially lacking the contraction rule) having infinitely many rule schemata, and no semantics was provided for it. We look in the present dissertation at the propositional fragment of ?, showing that it is algebraizable (in fact, implicative) in the sense of Blok and Pigozzi with respect to a class of involutive residuated lattices. We thus provide the first known algebraic semantics for ?(we call them of ?-algebras) as well as a finite Hilbert-style calculus equivalent to Nelson?s presentation. We provide an algorithm to make ?-algebras from ?-algebras or implicative lattices and we prove some results about the class of algebras which we have introduced. We also compare ? with other logics of the Nelson family, that is, ?3 and ?4.

Submitted by Setor de Tratamento da Informa??o - BC/PUCRS (tede2@pucrs.br) on 2015-07-20T11:50:24Z No. of bitstreams: 1 472408 - Texto Completo.pdf: 512200 bytes, checksum: 5f63e80e4169224eed290a1843d451b0 (MD5) / Made available in DSpace on 2015-07-20T11:50:24Z (GMT). No. of bitstreams: 1 472408 - Texto Completo.pdf: 512200 bytes, checksum: 5f63e80e4169224eed290a1843d451b0 (MD5) Previous issue date: 2015-03-27 / This is a qualitative research, a study case. As a question of research it poses the following problem: How are the different conceptions of logic inserted in the teaching practice of a mathematics teachers? group in High School? Its main objective is to understand the insertion of the different logic conceptions in the teaching practice of a group of mathematics teachers in High School. In order to achieve this goal, the following specific objectives are considered: (1) Identify the different logic conceptions of a group of mathematics teachers in High School; (2) Understand how these teachers realize the presence of logic in their pedagogical practice; and (3) Identify the different logic conceptions present in pedagogical support materials used by these teachers. In the theoretical background the following themes are approached: Philosophy and Logic; The several conceptions of logic (Aristotle, Russell, Bacon, Decarte); The teaching and learning of logic. Six teachers who hold a degree in mathematics, teachers in the three grades of High School and the analysis of pedagogical support materials was made by the teachers. The data were submitted to the Discursive Textual Analysis. From the analysis the following categories emerged: Conceptions of the teachers about logic, The presence of the Logic in the teaching practice and The several conceptions of logic and the teaching material. In the first category showed that this group of teachers there is certain difficulty of defining what logic is. The group presented three definitions of logic which are: (1) all and any way of thinking; (2) all that can be explained through reason; and (3) sets of arguments that we use to validate or invalidate knowledge. Therefore, to the teachers, logic is the built of a solid argumentation, with coherent thinking, well structured, in order to be able to infer on premises, concepts, problem-situations and the reality, being able to modify them in a conscious way, based on reason, determining its validity and its falsity. In the second category, it became evident that all the teachers, somehow, approach logic in their teaching practices. They affirm that there is little time to teach logic as a topic or content of the subject. What refers to the approach of logic in its pedagogical practices, I evinced that this teachers? group use logic in their classes when they work with demonstrations, either in Mathematics or Physics subjects, when they work the connectives, with combinatorial and probability analysis, in problem solving, set theory, validation of arguments, true and false, and in all and any situation in which the teachers and students need to argument, solve a problem solving situation and interfere in the world and its reality. And in the third category, we evince that the logical conceptions that appear are the Cartesian ones, being this the most present, the conception of Wittgenstein, the Aristotelian conception and the Russell conception. Although these logical conceptions are present in their materials, none of the teachers identified them in an explicit way. This is, they affirm the presence of logic in their materials, but they do not identify which of the conceptions is present in their books, notebooks or booklets. / A pesquisa ? de natureza qualitativa, do tipo estudo de caso. Tem como quest?o de pesquisa o seguinte problema: De que modo as diferentes concep??es de L?gica est?o inseridas na pr?tica docente de um grupo de professores de Matem?tica de Ensino M?dio? Tem por objeto geral compreender a inser??o das diferentes concep??es de L?gica na pr?tica docente de um grupo de professores de Matem?tica de Ensino M?dio. Para atingir esse objetivo, s?o considerados os seguintes objetivos espec?ficos: (1) identificar as diferentes concep??es de l?gica de um grupo de professores de matem?tica do Ensino M?dio; (2) compreender como esses professores percebem a presen?a da L?gica na sua pr?tica pedag?gica; e (3) Identificar as diferentes concep??es de L?gica presentes em materiais de apoio pedag?gico utilizado por esses professores. Na fundamenta??o te?rica s?o abordados os seguintes temas: Filosofia e L?gica; As diversas concep??es de L?gica (Arist?teles Russell, Bacon, Descartes e Wittgenstein); A import?ncia da L?gica nos processos de ensino e de aprendizagem de Matem?tica. Foram entrevistados seis professores licenciados em Matem?tica, docentes nas tr?s s?ries do Ensino M?dio e realizada a an?lise de materiais de apoio pedag?gico utilizados pelos professores. Os dados foram submetidos ? An?lise Textual Discursiva. Da an?lise emergiram as seguintes categorias: Concep??es dos professores sobre L?gica, A presen?a da L?gica na pr?tica docente e As diversas concep??es de L?gica presentes no material did?tico. Na primeira categoria evidenciou-se que neste grupo de professores h? uma certa dificuldade em definir o que ? l?gica. O grupo apresentou tr?s defini??es de l?gica que s?o: (1) toda e qualquer forma de pensar; (2) tudo que pode ser explicado por meio da raz?o; e (3) conjuntos de argumentos que utilizamos para validar ou invalidar um conhecimento. Portanto, para os professores, L?gica ? a constru??o de uma argumenta??o s?lida, com pensamentos coerentes, bem estruturados, de modo que possamos inferir sobre premissas, conceitos, situa??es-problema e a realidade, podendo modific?-las de modo consciente, baseado na raz?o, determinando a sua validade e falsidade. Na segunda categoria, evidenciou-se que todos os professores, de alguma forma, abordam a L?gica em suas pr?ticas docentes. Afirmam que h? pouco tempo para se ensinar a L?gica como um t?pico ou conte?do da mat?ria. No que se refere ? abordagem da L?gica em suas pr?ticas pedag?gicas evidenciou-se que este grupo de professores utiliza a L?gica em suas aulas ao trabalhar com demonstra??es, seja nas disciplinas de Matem?tica ou F?sica, ao trabalhar com conectivos, com An?lise Combinat?ria e Probabilidade, na resolu??o de problemas, na teoria de conjuntos, na valida??o de argumentos, e em toda e qualquer situa??o em que professores e alunos necessitem argumentar, resolver uma situa??o-problema e interferir no mundo e em sua realidade. E na terceira categoria evidenciou-se que as concep??es de L?gica presentes no material did?tico s?o as concep??es Cartesiana, sendo esta a mais presente, a concep??o de Wittgenstein, a concep??o Aristot?lica e a concep??o de Russell. Embora essas concep??es l?gicas estejam presentes em seus materiais, nenhum dos professores as identificou de forma expl?cita. Isto ?, afirmam a presen?a da l?gica em seus materiais, mas n?o identificam qual das concep??es est? presente em seus livros, cadernos ou apostilas.

Made available in DSpace on 2015-03-03T15:47:47Z (GMT). No. of bitstreams: 1 PatrickCAT_DISSERT.pdf: 4794202 bytes, checksum: 05088b21ff2be2b3c2ccec958e7e6b62 (MD5) Previous issue date: 2013-06-03 / Logic courses represent a pedagogical challenge and the recorded number of cases of failures and of discontinuity in them is often high. Amont other difficulties, students face a cognitive overload to understand logical concepts in a relevant way. On that track, computational tools for learning are resources that help both in alleviating the cognitive overload scenarios and in allowing for the practical experimenting with theoretical concepts. The present study proposes an interactive tutorial, namely the TryLogic, aimed at teaching to solve logical conjectures either by proofs or refutations. The tool was developed from the architecture of the tool TryOcaml, through support of the communication of the web interface ProofWeb in accessing the proof assistant Coq. The goals of TryLogic are: (1) presenting a set of lessons for applying heuristic strategies in solving problems set in Propositional Logic; (2) stepwise organizing the exposition of concepts related to Natural Deduction and to Propositional Semantics in sequential steps; (3) providing interactive tasks to the students. The present study also aims at: presenting our implementation of a formal system for refutation; describing the integration of our infrastructure with the Virtual Learning Environment Moodle through the IMS Learning Tools Interoperability specification; presenting the Conjecture Generator that works for the tasks involving proving and refuting; and, finally to evaluate the learning experience of Logic students through the application of the conjecture solving task associated to the use of the TryLogic / A disciplina de L?gica representa um desa o tanto para docentes como para discentes, o que em muitos casos resulta em reprova??es e desist?ncias. Dentre as dificuldades enfrentadas pelos alunos est? a sobrecarga da capacidade cognitiva para compreender os conceitos l?gicos de forma relevante. Neste sentido, as ferramentas computacionais de aprendizagem s?o recursos que auxiliam a redu??o de cen?rios de sobrecarga cognitiva, como tamb?m permitem a experi?ncia pr?tica de conceitos te?ricos. O presente trabalho prop?e uma tutorial interativo chamado TryLogic, visando ao ensino da tarefa de Demonstra??o ou Refuta??o (DxR) de conjecturas l?gicas. Trata-se de uma ferramenta desenvolvida a partir da arquitetura do TryOcaml atrav?s do suporte de comunica??o da interface web ProofWeb para acessar o assistente de demonstra??o de teoremas Coq. Os objetivos do TryLogic s?o: (1) Apresentar um conjunto de li??es para aplicar estrat?gias heur?sticas de an?lise de problemas em L?gica Proposicional; (2) Organizar em passo-a-passo a exposi ??o dos conte?dos de Dedu??o Natural e Sem?ntica Proposicional de forma sequencial; e (3) Fornecer aos alunos tarefas interativas. O presente trabalho prop?e tamb?m apresentar a nossa implementa??o de um sistema formal de refuta??o; descrever a integra??o de nossa infraestrutura com o Ambiente Virtual de Aprendizagem Moodle atrav?s da especi ca??o IMS Learning Tools Interoperability ; apresentar o Gerador de Conjecturas de tarefas de Demonstra??o e Refuta??o e, por m, avaliar a experi?ncia da aprendizagem de alunos de L?gica atrav?s da aplica??o da tarefa de DxR em associa??o ? utiliza??o do TryLogic

Submitted by Automa??o e Estat?stica (sst@bczm.ufrn.br) on 2016-01-20T20:41:23Z No. of bitstreams: 1 EvandoCarlosPessini_TESE.pdf: 1797248 bytes, checksum: e3b1bb46971f452029930068e9f8babf (MD5) / Approved for entry into archive by Arlan Eloi Leite Silva (eloihistoriador@yahoo.com.br) on 2016-01-21T18:18:20Z (GMT) No. of bitstreams: 1 EvandoCarlosPessini_TESE.pdf: 1797248 bytes, checksum: e3b1bb46971f452029930068e9f8babf (MD5) / Made available in DSpace on 2016-01-21T18:18:20Z (GMT). No. of bitstreams: 1 EvandoCarlosPessini_TESE.pdf: 1797248 bytes, checksum: e3b1bb46971f452029930068e9f8babf (MD5) Previous issue date: 2014-07-29 / Coordena??o de Aperfei?oamento de Pessoal de N?vel Superior - CAPES / Esta tese apresenta um m?todo de certifica??o de composi??es de servi?os web sem?nticos, o qual visa assegurar estaticamente sua corre??o funcional. O m?todo de certifica??o consiste em duas dimens?es de verifica??o, denominadas base e funcional. A dimens?o base ? centrada na verifica??o da correta aplica??o dos servi?os web sem?nticos na composi??o, i.e., visa certificar que as invoca??es de servi?o especificadas na composi??o est?o em conformidade com as respectivas defini??es dos servi?os. A certifica??o desta dimens?o explora a compatibilidade sem?ntica entre os argumentos dados na invoca??o e os par?metros formais do servi?o web sem?ntico. A dimens?o funcional visa certificar que a composi??o cumpre uma dada especifica??o expressa na forma de pr? e p?s-condi??es. Esta dimens?o ? formalizada atrav?s de um c?lculo baseado na l?gica de Hoare. Especifica??es de corre??o parciais envolvendo composi??es de servi?os web sem?nticos podem ser derivadas a partir do sistema dedutivo proposto. Este trabalho caracteriza-se tamb?m por explorar o emprego de um fragmento da l?gica descritiva, i.e., ALC, para expressar as especifica??es de corre??o parciais. Como forma de operacionalizar o m?todo de certifica??o, foi desenvolvido um ambiente de suporte para a defini??o das composi??es de servi?os web sem?nticos, assim como os mecanismos necess?rios para realizar a certifica??o. O m?todo de certifica??o foi avaliado experimentalmente atrav?s da aplica??o em tr?s provas de conceito diferentes. As provas de conceito desenvolvidas possibilitaram avaliar de forma ampla o m?todo de certifica??o proposto / This thesis presents a certification method for semantic web services compositions which aims to statically ensure its functional correctness. Certification method encompasses two dimensions of verification, termed base and functional dimensions. Base dimension concerns with the verification of application correctness of the semantic web service in the composition, i.e., to ensure that each service invocation given in the composition comply with its respective service definition. The certification of this dimension exploits the semantic compatibility between the invocation arguments and formal parameters of the semantic web service. Functional dimension aims to ensure that the composition satisfies a given specification expressed in the form of preconditions and postconditions. This dimension is formalized by a Hoare logic based calculus. Partial correctness specifications involving compositions of semantic web services can be derived from the deductive system proposed. Our work is also characterized by exploiting the use of a fragment of description logic, i.e., ALC, to express the partial correctness specifications. In order to operationalize the proposed certification method, we developed a supporting environment for defining the semantic web services compositions as well as to conduct the certification process. The certification method were experimentally evaluated by applying it in three different proof concepts. These proof concepts enabled to broadly evaluate the method certification

Submitted by Automa??o e Estat?stica (sst@bczm.ufrn.br) on 2016-07-26T00:34:28Z No. of bitstreams: 1 AlanSoaresBezerra_DISSERT.pdf: 1973624 bytes, checksum: be7c07504c6994ecc019750ef704dd90 (MD5) / Approved for entry into archive by Arlan Eloi Leite Silva (eloihistoriador@yahoo.com.br) on 2016-08-08T19:41:41Z (GMT) No. of bitstreams: 1 AlanSoaresBezerra_DISSERT.pdf: 1973624 bytes, checksum: be7c07504c6994ecc019750ef704dd90 (MD5) / Made available in DSpace on 2016-08-08T19:41:41Z (GMT). No. of bitstreams: 1 AlanSoaresBezerra_DISSERT.pdf: 1973624 bytes, checksum: be7c07504c6994ecc019750ef704dd90 (MD5) Previous issue date: 2016-03-18 / Coordena??o de Aperfei?oamento de Pessoal de N?vel Superior (CAPES) / O presente trabalho teve por objetivo compreender como o segmento gospel - tendo por base o Minist?rio de Louvor Diante do Trono, se articula ? l?gica de mercado por sua inser??o na ind?stria fonogr?fica e se utiliza da l?gica simb?lica nas can??es temas dos seus CDs/DVDs. Nossa pesquisa caracterizou-se por estudo de caso, constituindo-se metodologicamente pela an?lise descritiva do processo de produ??o, distribui??o e veicula??o dos CDs da banda e da an?lise funcional da m?sica que permeou toda a disserta??o. Como corpus anal?tico, as seguintes can??es temas dos CDs: Preciso de Ti, Quero me Apaixonar, Tua Vis?o, Creio, Tu Reinas e Tetelestai. Partimos da hip?tese que as institui??es religiosas, como campo detentor da estrutura??o de bandas e artistas gospel, vivenciam uma nova din?mica que consiste em uma modernidade de superf?cie ratificada nas formas de comunicar dos bens simb?licos produzidos, ou seja, simulam uma modernidade religiosa mantendo valores tradicionais quanto aos dogmas da religi?o, mas incorporam procedimentos empresariais e publicit?rios na divulga??o de seus produtos. Os resultados encontrados apontam para a m?sica gospel como media??o, integrante do ritual religioso, por vezes como ora??o e por outras como prega??o, estimulante de consumo e de entretenimento, e, desempenha a a??o de dispositivo na constru??o referencial de bens simb?licos. / This study aims to understand how the gospel music genre - based on the gospel band Minist?rio de Louvor Diante do Trono - articulates itself to the logic of the market by its insertion in the music industry and use of symbolic logic in the available songs of their Cds and DVDs. Our research is a case study, methodologically being the descriptive analysis of the production process, distribution and broadcasting of the band's CDs and functional analysis of the music that permeates the entire thesis. The following songs are presented as an analytical corpus: Preciso de Ti,Quero me Apaixonar, Tua Vis?o, Creio, Tu Reinas e Tetelestai. Our hypothesis is that religious institutions - as a field responsible for the structure which maintains gospel artists - experiences a new dynamic that consists of a superficial modernity, ratified in the ways the symbolic goods produced communicate, that is, simulate a religious modernity maintaining traditional values regarding the dogmas of religion , but incorporate business and advertising procedures in the dissemination of its products The results point to gospel music as mediation, part of the religious ritual sometimes as prayer and other as preaching, stimulating consumption and entertainment, and performing as a device in the making of symbolic goods.