nÃo hà / à papel preponderante da administraÃÃo tributÃria, supervisionar o integral cumprimento das obrigaÃÃes tributÃrias por parte dos contribuintes, cabendo aos seus agentes, quando se depararem com situaÃÃes caracterizadas como ilÃcitos fiscais, efetuarem o devido lanÃamento do crÃdito tributÃrio. A lavratura do auto de infraÃÃo à o ato administrativo atravÃs do qual se faz esse lanÃamento, devendo o mesmo, quando da sua elaboraÃÃo, atender a todos os requisitos legais, sob pena de nÃo cumprir com a sua finalidade. Por essa razÃo, elaborou-se esse estudo, na intenÃÃo de quantificar e identificar os principais vÃcios formais praticados quando da elaboraÃÃo dos Processos Administrativos TributÃrios, no Ãmbito da Secretaria da Fazenda do Estado do CearÃ. Como hipÃteses lanÃadas, esses erros sÃo o motivo principal pelo qual o Contencioso toma decisÃes contrÃrias à Fazenda Estadual, bem como os mesmos acontecem principalmente por desconhecimento, por parte do agente autuante, de dispositivos da norma regulamentadora da matÃria e que a quantidade de horas de capacitaÃÃo e de servidores treinados tem influÃncia direta na qualidade dos autos de infraÃÃo lavrados. Neste trabalho realizou-se um amplo levantamento bibliogrÃfico sobre a matÃria, bem como se utilizou relatÃrios do Contencioso Administrativo TributÃrio. Concluiu-se pela confirmaÃÃo da hipÃtese segundo a qual erros formais, na instauraÃÃo do Processo Administrativo TributÃrio, sÃo o principal motivo pelos quais os mesmos tÃm decisÃes por parte do Contencioso contrÃrias à Fazenda Estadual, nÃo se confirmando nesse trabalho, entretanto, a hipÃtese de que a quantidade de horas de capacitaÃÃo e de servidores treinados influi diretamente na qualidade dos autos de infraÃÃo lavrados. Resta tambÃm confirmado que os erros formais cometidos na elaboraÃÃo do PAT se dÃo principalmente por desconhecimento, por parte do agente fiscal, de dispositivos que regem a matÃria. / The tax administration has as preponderant role to oversee the full tax compliance by taxpayers, leaving it to their agents when faced with situations characterized as illegal tax, effect the release of the tax due. The issuance of the tax assessment is an administrative act through which makes this release, and the same should, when it is developed, to meet all legal requirements, otherwise they will not fulfill its purpose. Therefore, this study was drawn up, intending to quantify and identify the main formal defects practiced when preparing the Tax Administrative Procedure within the Department of Finance of the State of CearÃ. As hypotheses, these errors are the main reason why the litigation takes decisions against the State Treasury, and they occur mainly due to ignorance on the part of the active agent, the devices of the regulation of matter and the amount of hours training and trained servers directly influences the quality of violation reports issued. In this work we carried out a broad literature on the subject, and were used reports as the Administrative Litigation Tax. It was concluded by confirming the hypothesis that formal errors in the establishment of the Tax Administrative Process are the main reason why they are making by the litigation contrary to the State Treasury, not confirmed in this work, however, the hypothesis that number of hours of training and trained servers directly influences the quality of violation reports issued. It remains also confirmed that the formal errors committed in the preparation of PAT happen mainly due to ignorance on the part of the fiscal agent, the provisions governing the matter.

Neste trabalho apresentamos um modelo para ambientes inteligentes baseado em organizações de agentes, onde interações entre entidades são associadas a espaços físicos, pessoas carregam dispositivos e se movimentam entre diferentes espaços físicos e cada espaço físico contém definições de interações (comportamentos definidos por normas) próprias do seu contexto. São definidos três componentes deste modelo: (1) modelo conceitual, (2) linguagem de especificação e (3) ambiente de execução. A separação do modelo nestes três componentes traz como principais conseqüências: (1) a ativação de um ambiente inteligente é feita através de um mecanismo de alto nível, (2) a especificação de um ambiente inteligente é independente do domínio de aplicação e (3) as especificações podem ser executadas em mecanismos diferentes de execução. / We introduce a conceptual model for smart environments based on agent organizations where interactions between entities are associated with physical spaces, people (carrying mobile devices) move between different physical spaces and these physical spaces contain definitions of interactions (behaviors defined by norms) related to each context. This model defines three components: (1) conceptual model, (2) language specification, and (3) execution environment. The separation in these three components brings as main consequences: (1) activation of a smart environment is performed through a high-level mechanism, (2) specification of a smart environment is independent of the application domain, and (3) specifications can be performed on different mechanisms of execution.

Orientador: Ricardo de Oliveira Anido / Dissertação (mestrado) - Universidade Estadual de Campinas, Instituto de Computação / Made available in DSpace on 2018-08-10T11:44:38Z (GMT). No. of bitstreams: 1 SoaresJunior_JurandyMartins_M.pdf: 1209765 bytes, checksum: d8d6bebdcb7b65ed4a9fdb7e84508766 (MD5) Previous issue date: 2006 / Resumo: Testar um subsistema embarcado em um sistema complexo, assumindo-se que os demais subsistemas são livres de falhas, é conhecido como teste de conformidade em contexto. A complexidade deste teste reside no fato do subsistema mais externo, conhecido como contexto, ocultar muitas interações e eventos nos quais o sistema embarcado, conhecido como componente, participa. Nas últimas décadas alguns algoritmos foram desenvolvidos para resolver o problema. Muitos deles, no entanto, ignoram as condições nas quais podem ser aplicados. Nesta dissertação estudamos a teoria e os algoritmos relacionados a teste de conformidade e a teste de conformidade em contexto, propomos uma nova abordagem guiada por casos de teste do componente e analisamos as condições necessárias e suficientes para aplicá-Ia. A validação das condições necessárias e suficientes foi feita em estudos de casos com a pilha de protocolos do TCP/IP, com os protocolos HTTP e HTTPS via Proxy e com DHCP via relay-agent. Os algoritmos estudados foram experimentados nas especificações dos protocolos ABP, SCU e TCP / Abstract: Testing a subsystem embedded into a complex system, in which the other subsystems are assumed to be fault-free, is known as confonnance testing in contexto The complexity behind this test resides in the fact that the most external system, known as context, hides many interactions and events in which the embedded subsystem, known as component, participates. In the last decades some algorithms were developed to solve the problem. Many of them, however, ignore the conditions under which they can be applied. In this dissertation we study the theory and the algorithms related to confonnance testing and conformance testing in context, we propose a new approach guided by component's test cases, and we analyze the necessary and sufficient conditions to apply it. The validation of the necessary and sufficient conditions was done in case studies with the TCP/IP protocol stack, with the protocols HTTP and HTTPS . via Proxy, and with DHCP via relay-agent. The algorithms studied were experimented in the specifications of protocols ABP, seu e TCP / Mestrado / Engenharia de Protocolos / Mestre em Ciência da Computação

Made available in DSpace on 2014-06-12T16:00:15Z (GMT). No. of bitstreams: 2 arquivo6285_1.pdf: 1527923 bytes, checksum: 78d4cb768e2160db1bd4ea015fdefa03 (MD5) license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5) Previous issue date: 2007 / Sistema Embarcado ¶e um sistema computacional projetado para uma fun»c~ao dedicada. Geralmente, este sistema executa uma tarefa espec¶³¯ca dentre um conjunto maior de tarefas, e possui particularidades tanto de hardware quanto de software. Os Sistemas Embarcados est~ao presentes no cotidiano sob diferentes formas e com diferentes objetivos. Geralmente possuem uma s¶erie de restri»c~oes, tais como: dimens~oes das mem¶orias, fonte de energia, baixa velocidade de processamento, dentre outras. Este trabalho apresenta o desenvolvimento de um modelo em Redes de Petri de desem- penho e energias para c¶odigos ANSI-C, considerando um processador de uma plataforma embarcada espec¶³¯ca, com o objetivo de estimar o consumo de energia. A linguagem ANSI-C, como c¶odigo de Sistemas Embarcados, foi escolhida por ser uma das mais utilizadas no desenvolvimento destes sistemas. Redes de Petri Temporizadas permitem a modelagem e especi¯ca»c~ao de sistemas paralelos e distribu¶³dos e, ao mesmo tempo, prov^eem o formalismo matem¶atico necess¶ario para uma avalia»c~ao de desempenho. Neste trabalho, o modelo Redes de Petri Temporizada ¶e anotado com informa»c~ao de consumo de energia, o que originou a Power Petri Net. Este trabalho contribui tamb¶em com a implementa»c~ao de um simulador estoc¶astico para avalia»c~ao de desempenho e de um ambiente computacional no qual s~ao realizadas as estimativas. Esse ambiente ¶e formado pelo tradutor de c¶odigo ANSI-C para Redes de Petri no formato PNML [1], padr~ao XML para descri»c~ao de Redes de Petri, simulador estoc¶astico e extens~ao do ambiente EzPetri [2]. Como o modelo apresentado, b¶asico, pode ser estendido em outros trabalhos ¶e caracterizada a forma»c~ao de um framework. Para valida»c~ao do m¶etodo proposto, foi utilizado um c¶odigo de avalia»c~ao, benchmark, PowerStone [3] desenvolvido para explorar o sistema sob diferentes aspectos de consumo de energia

Orientador: Marcelo Esteban Coniglio / Tese (doutorado) - Universidade Estadual de Campinas, Instituto de Filosofia e Ciências Humanas / Made available in DSpace on 2018-08-17T19:11:26Z (GMT). No. of bitstreams: 1 Silvestrini_LuizHenriquedaCruz_D.pdf: 1289416 bytes, checksum: aa5f4929e7149a647d28c4fd4df86874 (MD5) Previous issue date: 2011 / Resumo: Mikenberg, da Costa e Chuaqui (1986) introduziram a noção de quase-verdade por meio da noção de estruturas parciais, e para tanto, conceberam os predicados como ternas. O arcabouço conceitual resultante proporcionou o emprego de estruturas parciais na ciência, pois, em geral, não sabemos tudo a respeito de um determinado domínio de conhecimento. Generalizamos a noção de predicados como ternas para fórmulas complexas. A partir desta nova abordagem, obtemos uma definição de quase-verdade via noção de satisfação pragmática de uma fórmula A em uma estrutura parcial E. Introduzimos uma lógica subjacente à nossa nova definição de quase-verdade, a saber, a lógica paraconsistente trivalente LPT1, a qual possui uma axiomática de primeira ordem. Relacionamos a noção de quase-verdade com algumas lógicas paraconsistentes já existentes. Defendemos que a formalização das Sociedades Abertas, introduzidas por Carnielli e Lima-Marques (1999), quando combinada com quantificadores modulados, introduzidos por Grácio (1999), constitui uma alternativa para capturar a componente indutiva presente na atividade científica, e mostramos, a partir disso, que a proposta original de da Costa e colaboradores pode ser explicada em termos da nova noção de sociedades moduladas / Abstract: Newton da Costa and his collaborators have introduced the notion of quasi-truth by means of partial structures, and for this purpose, they conceived the predicates as ordered triples: the set of tuples which satisfies, does not satisfy and can satisfy or not the predicate, respectively (the latter represents lack of information). This approach provides a conceptual framework to analyse the use of (first-order) structures in science in contexts of informational incompleteness. In this Thesis, the notion of predicates as triples is extended recursively to any complex formula of the first-order object language. From this, a new definition of quasi-truth via the notion of pragmatic satisfaction is obtained. We obtain the proof-theoretic counterpart of the logic underlying our new definition of quasi-truth, namely, the three-valued paraconsistent logic LPT1, which is presented axiomatically in a first-order language. We relate the notion of quasi-truth with some existing paraconsistent logics. We defend that the formalization of (open) society semantics when combined with the modulated quantifiers constitutes an alternative to capture the inductive component present in scientific activity, and show, from this, that the original proposal of da Costa and collaborators can be explained in terms of the new concept of modulated societies / Doutorado / Filosofia / Doutor em Filosofia

Made available in DSpace on 2015-04-11T14:03:15Z (GMT). No. of bitstreams: 1 DISSERTACAO MARCELO.pdf: 1313111 bytes, checksum: ddf9a22433355413e807d3bd27951a01 (MD5) Previous issue date: 2008-12-15 / Fundação de Amparo à Pesquisa do Estado do Amazonas / Embedded systems have undeniable relevance in modern society. They have temporal constraints (as long as they are real time ones), power consumption management, size, weight, etc which make their design more complex than the design of their desktop peers. Given the huge number of requirements of all kinds, the high complexity of embedded software as well as the big possibilities of critical damages in case of flaws and, at last, the even bigger pressure of market for new products faster, it make necessary methods which can assure correct, fast but intuitive specification and conception of designs. Considering this, this work aims to provide a method which contribute to the state of art. The goal of the proposed method is to provide an approach which gather an specification of an embedded software in a semi-formal, object-oriented and Industry-accepted notation, which is Unified Modeling (UML), specifically their Sequence Diagram notation which is able to capture dynamic aspects of a system and a mecanism of translation of this notation into a formal one, called SMV, apropriate for being used by the SMV model checker. The goal of the method is also provide an translation scheme of the sequence diagrams into another formal notation, the so called Petri Nets notations. Petri Net notation is well suited to formal verification. Finally, the goal of the method is to provide a mechanism of translation of high level properties queries into formal notation CTL. Property queries are only qualitative. All these functionalities are implemented in a tool called Ambiente de Verificação Formal de Software Embarcado. / Os sistemas embarcados possuem inegável importância na sociedade atual. Eles possuem restrições temporais (quando são de tempo real), de gerência de consumo de energia, tamanho, peso etc que tornam o seu projeto e concepção mais complexos do que os sistemas convencionais. Dado o grande número de requisitos de todos os tipos, a alta complexidade dos softwares embarcados desenvolvidos bem como a grande possibilidade de catástrofes significativas em caso de falha e por fim a grande pressão de mercado por produtos cada vez mais rápido, fazem-se necessários métodos que possam assegurar uma correta, rápida porém intuitiva especificação e concepção dos projetos. Diante disso, o presente trabalho visa prover um método que acrescente ao atual estado da arte. O objetivo do método então é prover uma abordagem que colete uma especificação de software embarcado em uma notação semi-formal, orientada a objetos e amplamente aceita pela Indústria, que é a Unified Modeling Language (UML), especificamente com seu Diagrama de Sequência, o qual é apto para capturar os aspectos dinâmicos de um sistema e um mecanismo de tradução dessa notação para a notação formal SMV, apta a ser utilizada pelo model checker de mesmo nome. O objetivo do método é prover também um esquema de tradução dos diagramas de sequência em UML para uma notação formal, no caso a notação de Redes de Petri, o qual é adequada para verificação formal, gerando saídas de arquivos nos formatos APNN e PNML. O formato APNN é adequado para ser usado no Model Checking Kit (MCK). Por fim, prover um esquema de tradução consultas de propriedade em alto nível para o formato de CTL puro adequado para ser usado no MCK e um programa em SMV e sua especificação 7 em CTL, formatos aptos a serem usados no model checker SMV. A verificação de propriedades é apenas qualitativa, isto é, que verificará apenas propriedades de execução do software embarcado, em oposição às propriedades quantitativas de tempo por exemplo, comuns em softwares de tempo-real. Todas essas funcionalidades são realizadas por uma ferramenta, chamada Ambiente de Verificação Formal de Software Embarcado.

Submitted by Franciele Moreira (francielemoreyra@gmail.com) on 2018-02-15T15:02:41Z No. of bitstreams: 2 Dissertação - Thiago de Almeida Bastos -2018 .pdf: 2834099 bytes, checksum: 20704146dd6e29dc70c067fcbd0011a2 (MD5) license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) / Approved for entry into archive by Luciana Ferreira (lucgeral@gmail.com) on 2018-02-16T09:38:12Z (GMT) No. of bitstreams: 2 Dissertação - Thiago de Almeida Bastos -2018 .pdf: 2834099 bytes, checksum: 20704146dd6e29dc70c067fcbd0011a2 (MD5) license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) / Made available in DSpace on 2018-02-16T09:38:12Z (GMT). No. of bitstreams: 2 Dissertação - Thiago de Almeida Bastos -2018 .pdf: 2834099 bytes, checksum: 20704146dd6e29dc70c067fcbd0011a2 (MD5) license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) Previous issue date: 2018-01-30 / This master's thesis seeks to contribute to the automation of production lines, and proposes a methodology for the formal verification of flexible manufacturing models by the Petri-PDL tool. The Petri-PDL framework is based on a multimodal logic associated with a scheme defined for the problem with the Petri nets to specify and model sequential problems demonstrating in logical proofs the correctness of properties inferred by the model. This formal treatment is adapted for the treatment of flexible sequential processes, since these models are used in many other applications with Petri nets. They will be considered models of flexible production system found in the systematic review to evaluate the efficiency of its model and its adaptation to this formal refinement. / Este trabalho busca contribuir com a automação de linhas de produção e propõe uma metodologia para a verificação formal de modelos de manufatura flexível a partir da ferramenta Petri-PDL. O conceito Petri-PDL baseia-se em uma lógica multimodal associada ao esquema definido para o problema com as redes de Petri para especificar e modelar problemas sequenciais demonstrando em provas lógicas a corretude de propriedades inferidas pelo modelo. Este tratamento formal será adaptado para o tratamento de processos sequenciais flexíveis, uma vez que estes modelos são usados em muitas outras aplicações com redes de Petri. Serão considerados modelos de sistema de produção flexível encontrados na revisão sistemática para avaliar a eficiência de seu modelo e sua adaptação a este refinamento formal.

A Análise de Conceitos Formais (FCA) é uma teoria matemática que formaliza a noção de conceitos e hierarquias conceituais. De importância central a esta teoria é uma estrutura algébrica denominada reticulado de conceitos. Esta estrutura é definida em função de um conjunto de objetos, outro de atributos e uma relação que indica os atributos apresentados por cada objeto. Uma representação gráfica de um reticulado de conceitos, por meio de uma interface computacional, é capaz de expor regularidades presentes em dados a um usuário, e este pode então realizar tarefas de análise exploratória de dados. Este tipo de aplicação de FCA vem sendo empregado em dezenas de projetos pertencentes a áreas diversas, como medicina, serviços de inteligência, engenharia de software e bioinformática. Mostramos neste trabalho um sistema de análise exploratória de dados baseado em FCA, e sua utilização sobre dados reais. Também é mostrado como reticulados de conceitos podem ser empregados em interfaces de recuperação de informação. Do ponto de vista algorítmico, analisamos métodos computacionais para a determinação do reticulado de conceitos, e também de uma subestrutura simplificada, o conjunto de conceitos. O tamanho de um reticulado de conceitos pode ser exponencial em função dos tamanhos dos conjuntos de objetos e de atributos. Assim, é de vital interesse o estabelecimento de cotas superiores para o número de conceitos de um reticulado. Neste trabalho, apresentamos as cotas já conhecidas presentes na literatura. Também estabelecemos uma nova cota superior, e mostramos famílias de casos em que nossa cota superior é mais justa que as demais. Para algumas famílias particulares, nossa cota é polinomial, enquanto que as demais são exponenciais. / Formal Concept Analysis (FCA) is a mathematical theory that formalizes the notion of concepts and conceptual hierarchies. Of central importance to this theory is an algebraic structure termed concept lattice. Such structure becomes defined after being given one set of objects, one of attributes, and an incidence relation describing the attributes held by each object. A graphical representation of a concept lattice, by means of a computational interface, is capable of unfolding regularities present in data to an user, who is then able to conduct exploratory data analysis tasks. This sort of FCA application is currently deployed in tens of projects belonging to a wide range of areas, such as medicine, intelligence services, software engineering and bioinformatics. We show in this work an FCA-based system of exploratory data analysis, and its use over real data. Moreover, it is shown how concept lattices can be employed in information retrieval interfaces. From the algorithmic viewpoint, we analyse computational methods for the determination of a concept lattice, and also of a simplified substructure, the concept set. The size of a concept lattice can be exponential when compared to the size of the objects and the attributes sets. Therefore, it is of paramount interest the establishment of upper bounds for the number of concepts of a lattice. In this work, we present the upper bounds already known in the literature. We also establish a new upper bound, and show families of cases in which our bound is sharper than the others. For particular families, our bound is polynomial, whereas the other bounds are exponential.

Orientador: Charlotte Marie Chambelland Galves / Dissertação (mestrado) - Universidade Estadual de Campinas, Instituto de Estudos da Linguagem / Made available in DSpace on 2018-08-20T16:18:53Z (GMT). No. of bitstreams: 1 Macedo-Costa_Tatiane_M.pdf: 3956141 bytes, checksum: 4d252c5e128eda2fc8db54185242f443 (MD5) Previous issue date: 2012 / Resumo: Essa dissertação investiga, sob a perspectiva da linha gerativista diacrônica, as variadas realizações do objeto direto anafórico no Português Brasileiro, mais especificamente, no dialeto baiano, em textos jornalísticos publicados em periódicos que circularam na cidade de Salvador (BA). O corpus da pesquisa foi composto por sete jornais, distribuídos em três épocas distintas: de 1833 a 1850 (Diário da Bahia, Novo Diário da Bahia e O Atheneo), de 1898 a 1900 (Correio de Notícias e Jornal de Notícias) e de 1945 a 1948 (Diário da Bahia e Diário de Notícias). A partir da constatação obtida por diversos estudos sincrônicos (cf. Duarte (1986), Corrêa (1991), Averbug (2000), Magalhães (2006)), e diacrônicos (cf. Cyrino (1994)) de que há um aumento do uso de uma categoria vazia na posição de objeto em Português Brasileiro em decorrência da diminuição do uso de clíticos, objetivamos investigar as formas de realização do objeto direto anafórico em textos formais, no intuito de identificar se, nesse tipo de texto, tal mudança também se evidenciaria. Além de analisar as variadas estratégias de realização dessa posição, examinamos também os fatores que as condicionam, uma vez que estes também sofreram mudança ao longo do tempo (cf. Cyrino (1994), Figueiredo (2009)). A análise dos dados revelou que a mudança atestada nos estudos supracitados também se verifica na análise dos textos formais, apesar do seu caráter conservador e a despeito da norma culta influenciar o uso de determinadas formas gramaticais na escrita. Além de um aumento dos objetos nulos nos dados em detrimento do uso dos clíticos, a análise dos condicionamentos linguísticos mostrou que essa categoria tem sido utilizada ao longo do tempo em contextos cada vez menos restritos, sendo favorecida apenas pela correspondência sintática entre essa variante e o seu DP antecedente/ referente / Abstract: This dissertation investigates, from a diachronic generative perspective, the varied uses of the anaphoric direct object in Brazilian Portuguese, more specifically, in the dialect spoken in Bahia, in journalistic texts published in periodicals that circulated in Salvador (BA). The corpus of this research was composed by seven newspapers, distributed across three distinct periods: from 1833 to 1850 (Diário da Bahia, Novo Diário da Bahia and O Atheneo), 1898 to 1900 (Correio de Notícias and Jornal de Notícias) and 1945 to 1948 (Diário da Bahia and Diário de Notícias). From the finding obtained from various synchronic and diachronic studies (cf. Duarte (1986), Corrêa (1991), Cyrino (1994), Averbug (2000), Magalhães (2006)) that there is an increase in the use of an empty category in position of the object in Brazilian Portuguese, as a result of the declining use of clitics, we aim to investigate the ways to perform the anaphoric direct object in formal texts, in order to identify whether, in this type of text, such change would also be evident. Besides analyzing the various strategies of performing this position, we also examined the factors that influence them, since these factors also suffered change over time (cf. Cyrino (1994), Figueiredo (2009)). The data analysis revealed that the change attested on the mentioned studies also applies to the analysis of formal texts, despite of its conversationalist character and in spite of the standard use of language influences the use of certain grammatical forms in the writing. Besides an increase of null objects in the data over the use of clitics, the analysis of linguistic conditioning showed that this category has been used over time in contexts less and less restricted, being favored only by syntactic correspondence between this variant and its antecedent/referent DP / Mestrado / Linguistica / Mestre em Linguística

Orientador: Maria de Lourdes Spazziani / Resumo: Esta pesquisa objetivou analisar, segundo alguns pressupostos da Teoria Histórico-Cultural de Vigotski e da Educação Ambiental, os limites e/ou potencialidades de um processo formativo de monitores, desenvolvido em um espaço não formal de ensino. De natureza qualitativa, a pesquisa teve como sujeitos estudantes do Ensino Médio, da rede pública estadual de ensino, participantes do projeto Clube da Mata que concluíram um processo formativo, composto por curso de formação e atuação em monitorias, oferecidas a estudantes dos anos iniciais do Ensino Fundamental. Esta formação ocorreu na Fazenda Experimental São Manuel, mediante a parceria entre a Prefeitura Municipal de São Manuel, cidade do interior do estado de São Paulo, e a Unesp, campus de Botucatu. Com o intuito de verificar a sua contribuição para a ampliação e/ou modificação de concepções, perspectivas e ações socioambientais destes monitores, os instrumentos de coleta de dados foram questionários impressos, com questões abertas, e entrevistas semiestruturadas. Para tanto, a coleta foi realizada em três etapas distintas: aplicação de questionário aos participantes antes da realização do curso, tendo um caráter diagnóstico; aplicação de questionário aos participantes após o curso, tendo um caráter comparativo; e, entrevista com os participantes que atuaram como monitores voluntários. Os dados obtidos foram analisados por meio da técnica Análise Temática do método Análise de Conteúdo, segundo o desenvolvimento proposto por B... (Resumo completo, clicar acesso eletrônico abaixo) / Mestre