CCET - DM - Artigos publicados em periódicos
URI Permanente para esta coleçãohttps://repositorio.ufrn.br/handle/1/2985
Navegar
Submissões Recentes
Artigo Equações do segundo grau e mudança de variáveis(Revista Ciências e Natura, 2015) Silva, Márcio Vieira da; Pereira, Andre Gustavo CamposEsse artigo apresentará parte de uma Dissertação de Mestrado (Profmat, 2014), que buscou auxiliar na melhoria da prática pedagógica do professor de matemática, pratica essa que nos últimos anos deixou de ser também investigativa e passou a ser bastante mecânica, isso fica evidente a partir do estudo de Álgebra do Ensino Fundamental, sobretudo no tema equações do segundo grau. Tema este que na maioria dos livros didáticos brasileiros, é abordado sem nenhum contexto histórico, apresentam duas ou três técnicas de resolução além de que o aluno que não consegui com desenvoltura aprender radiciação e potenciação ficará fadado a nunca conseguir determinar as raízes de tais equações, sendo assim este artigo apresentará uma mudança de variável que facilita a determinação das raízes de equações do segundo grauArtigo Sinais e sistemas definidos sobre aritmética intervalar complexa(Sociedade Brasileira de Matemática Aplicada e Computacional, 2012-03-17) Santana, Fabiana Tristão de; Santana, Fágner Lemos; Doria Neto, Adrião Duarte; Santiago, Regivan Hugo NunesNeste trabalho, é feita a fundamentação para os conceitos de sinais e sistemas intervalares complexos, fazendo-se o uso da aritmética complexa retangular e do conceito de intervalo de números complexos feito com auxílio da chamada ordem de Kulisch-Miranker para complexos. É apresentado também o conceito de representação intervalar e é definida a representação canônica intervalar (CIR) de funções complexas. A partir de um sistema f que opere sobre sinais cujos valores sejam números complexos, usando a função CIR, encontra-se um sistema intervalar F o qual preserva, no ambiente intervalar, as propriedades de f, tais como estabilidade, invariância no tempo, aditividadade, homogeneidade e linearidadeArtigo Uma abordagem interdisciplinar para obtenção da melhor função aproximada para ajuste de dados(Brazilian Journal of Development, 2019-10-01) Santana, Fabiana Tristão de; Marcone, Marcos Henrique Fernandes; Santana, Fágner Lemos deNeste trabalho, importantes conceitos das Ciências Exatas, Computação e Engenharias atuam de forma interdisciplinar para obter a melhor solução aproximada para um experimento físico. O objetivo do trabalho é mostrar como diferentes teorias podem ser usadas para solucionar problemas nas Engenharias. Mais especificamente, serão utilizados aqui o método de Mínimos Quadrados (estudado na Álgebra Linear), as incertezas e operações intervalares (estudados na Matemática Intervalar) e a linguagem Python (estudada na computação) para resolver um sistema intervalar que fornece a melhor função aproximada que ajusta um conjunto de dados oriundos de um experimento físico, no qual um carro se deslocava com aceleração nula sob um trilho de ar horizontal. Ao fazer esse tipo de abordagem usando a Matemática Intervalar, busca-se inferir como as incertezas provenientes do experimento, assim como os erros gerados pelas representações e operações dos números em computadores, interferem no resultado obtido. Para isso, se fez necessário a utilização da biblioteca Python for Extended Scientific Computing (Python-XSC), a qual é baseada na estrutura da aritmética intervalar e fornece funções para a resolução de sistemas lineares intervalares. A aplicação do estudo feito se mostrou bastante eficiente e de fácil utilização, além de estimular os estudantes de engenharia a buscarem soluções inovadoras através da interdisciplinaridade das teorias estudadas na áreaArtigo Inovação no processo de ensino e aprendizagem de álgebra linear usando o software geogebra(Brazilian Journal of Development, 2019-09-16) Santana, Fabiana Tristão de; Macedo, Igor Michael Araujo de; Marcone, Marcos Henrique Fernandes; Santana, Fágner Lemos deEste trabalho aborda estratégias pedagógicas aplicadas na disciplina de Álgebra Linear utilizando o software educativo GeoGebra para inovar o processo de ensino e aprendizagem de alguns temas específicos, como: vetores, matrizes, projeções ortogonais e o método dos mínimos quadrados. O tratamento desses e de outros tópicos utilizando o software GeoGebra é feito especificamente na Janela CAS (ambiente de programação com uma linguagem simples e acessível a todos os estudantes), Janela de Visualização (ambiente de esboços gráficos em duas e três dimensões) e Janela de Álgebra (ambiente de edição e armazenamento de escalares, funções, vetores e variáveis definidos). Os principais comandos utilizados no estudo desses tópicos serão apresentados juntamente com a resolução e análise gráfica de três sistemas lineares. Para finalizar, o método dos mínimos quadrados será utilizado e implementado no software com o objetivo de encontrar a melhor função que ajusta um conjunto de dados experimentais obtidos em laboratório de física. O uso do software no ensino da Álgebra Linear tem ajudado os estudantes a compreenderem melhor alguns conceitos trabalhados na sala de aula, além de deixar o estudo mais prazeroso e interessanteArtigo A proof theoretic study of soft concurrent constraint programming(Cambridge University Press, 2014) Pimentel, Elaine Gouvea; Nigam, Vivek; Vega, Carlos Alberto OlarteConcurrent Constraint Programming (CCP) is a simple and powerful model for concurrency where agents interact by telling and asking constraints. Since their inception, CCP-languages have been designed for having a strong connection to logic. In fact, the underlying constraint system can be built from a suitable fragment of intuitionistic (linear) logic -ILL- and processes can be interpreted as formulas in ILL. Constraints as ILL formulas fail to represent accurately situations where “preferences” (called soft constraints) such as probabilities, uncertainty or fuzziness are present. In order to circumvent this problem, c-semirings have been proposed as algebraic structures for defining constraint systems where agents are allowed to tell and ask soft constraints. Nevertheless, in this case, the tight connection to logic and proof theory is lost. In this work, we give a proof theoretical meaning to soft constraints: they can be defined as formulas in a suitable fragment of ILL with subexponentials (SELL) where subexponentials, ordered in a c-semiring structure, are interpreted as preferences. We hence achieve two goals: (1) obtain a CCP language where agents can tell and ask soft constraints and (2) prove that the language in (1) has a strong connection with logic. Hence we keep a declarative reading of processes as formulas while providing a logical framework for soft-CCP based systems. An interesting side effect of (1) is that one is also able to handle probabilities (and other modalities) in SELL, by restricting the use of the promotion rule for non-idempotent c-semirings.This finer way of controlling subexponentials allows for considering more interesting spaces and restrictions, and it opens the possibility of specifying more challenging computational systemsArtigo Dynamic spaces in concurrent constraint programming(Elsevier, 2014) Nigam, Vivek; Pimentel, Elaine Gouvea; Vega, Carlos Alberto OlarteConcurrent constraint programming (CCP) is a declarative model for concurrency where agents interact with each other by posting (telling) and asking constraints (formulas in logic) in a shared store of partial information. With the advent of emergent applications as security protocols, social networks and cloud computing, the CCP model has been extended in different directions to faithfully model such systems as follows: (1) It has been shown that a name-passing discipline, where agents can communicate local names, can be described through the interplay of local (∃) processes along with universally (∀) quantified asks. This strategy has been used, for instance, to model the generation and communication of fresh values (nonces) in mobile reactive systems as security protocols; and (2) the underlying constraint system in CCP has been enhanced with local stores for the specification of distributed spaces. Then, agents are allowed to share some information with others but keep some facts for themselves. Recently, we have shown that local stores can be neatly represented in CCP by considering a constraint system where constraints are built from a fragment of linear logic with subexponentials (SELL). In this paper, we explore the use of existential (⋓) and universal (⋒) quantification over subexponentials in SELL in order to endow CCP with the ability to communicate location (space) names. The resulting CCP language that we obtain is a model of distributed computation where it is possible to dynamically establish new shared spaces for communication. We thus extend the sort of mobility achieved in (1) –for variables – to dynamically change the shared spaces among agents – (2) above. Finally, we argue that the new CCP language can be used in the specification of service oriented computing systemsArtigo Subexponential concurrent constraint programming(Elsevier, 2015) Pimentel, Elaine Gouvea; Nigam, Vivek; Vega, Carlos Alberto OlarteIn previous works we have shown that linear logic with subexponentials (SELL), a refinement of linear logic, can be used to specify emergent features of concurrent constraint programming (CCP) languages, such as preferences and spatial, epistemic and temporal modalities. In order to do so, we introduced a number of extensions to SELL, such as subexponential quantifiers for the specification of modalities, and more elaborated subexponential structures for the specification of preferences. These results provided clear proof theoretic foundations to existing systems. This paper goes in the opposite direction, answering positively the question: can the proof theory of linear logic with subexponentials contribute to the development of new CCP languages? We propose a CCP language with the following powerful features: 1) computational spaces where agents can tell and ask preferences (soft-constraints); 2) systems where spatial and temporal modalities can be combined; 3) shared spaces for communication that can be dynamically established; and 4) systems that can dynamically create nested spaces. In order to provide the proof theoretic foundations for such a language, we propose a unified logical framework (SELLS) combining the extensions of linear logic with subexponentials mentioned above, and showing that this new framework has interesting proof theoretical properties such as cut-elimination and a sound and complete focused proof systemArtigo Proving concurrent constraint programming correct, revisited(Elsevier, 2015) Vega, Carlos Alberto Olarte; Pimentel, Elaine GouveaConcurrent Constraint Programming (CCP) is a simple and powerful model of concurrency where processes interact by telling and asking constraints into a global store of partial information. Since its inception, CCP has been endowed with declarative semantics where processes are interpreted as formulas in a given logic. This allows for the use of logical machinery to reason about the behavior of programs and to prove properties in a declarative way. Nevertheless, the logical characterization of CCP programs exhibits normally a weak level of adequacy since proofs in the logical system may not correspond directly to traces of the program. In this paper, relying on a focusing discipline, we show that it is possible to give a logical characterization to different CCP-based languages with the highest level of adequacy. We shall also provide a neater way of interpreting procedure calls by adding fixed points to the logical structureArtigo From cut-free calculi to automated deduction: the case of bounded contraction(Elsevier, 2017) Ciabattoni, Agata; Lellmann, Bjorn; Vega, Carlos Alberto Olarte; Pimentel, Elaine GouveaThe addition of the bounded contraction rules to Full Lambek Calculus with exchange and weakening (FLew) gives rise to serious complications for proof search. For example, adding to FLew a naive version of these rules brakes cut-admissibility. Although this can be avoided by refining these rules, in this work we show that even “good” proof systems for FLew plus bounded contraction do not necessarily lead to good implementations. In order to solve this problem, we propose an extension of the lazy splitting methodology to bounded contractions, showing how to transform our focused, cut-free sequent calculus into a terminating theorem prover. Our system is used to show that the decision problem for FLew with bounded contraction is in EXPTIMEArtigo Hybrid and subexponential linear logics(Elsevier, 2017) Despeyroux, Joelle; Pimentel, Elaine Gouvea; Vega, Carlos Alberto OlarteHyLL (Hybrid Linear Logic) and SELL (Subexponential Linear Logic) are logical frameworks that have been extensively used for specifying systems that exhibit modalities such as temporal or spatial ones. Both frameworks have linear logic (LL) as a common ground and they admit (cut-free) complete focused proof systems. The difference between the two logics relies on the way modalities are handled. In HyLL, truth judgments are labelled by worlds and hybrid connectives relate worlds with formulas. In SELL, the linear logic exponentials (!, ?) are decorated with labels representing locations, and an ordering on such labels defines the provability relation among resources in those locations. It is well known that SELL, as a logical framework, is strictly more expressive than LL. However, so far, it was not clear whether HyLL is more expressive than LL and/or SELL. In this paper, we show an encoding of the HyLL's logical rules into LL with the highest level of adequacy, hence showing that HyLL is as expressive as LL. We also propose an encoding of HyLL into SELL (SELL plus quantification over locations) that gives better insights about the meaning of worlds in HyLL. We conclude our expressiveness study by showing that previous attempts of encoding Computational Tree Logic (CTL) operators into HyLL cannot be extended to consider the whole set of temporal connectives. We show that a system of LL with fixed points is indeed needed to faithfully encode the behavior of such temporal operatorsArtigo On concurrent behaviors and focusing in linear logic(Elsevier, 2017) Vega, Carlos Alberto Olarte; Pimentel, Elaine GouveaConcurrent Constraint Programming (CCP) is a simple and powerful model of concurrency where processes interact by telling and asking constraints into a global store of partial information. Since its inception, CCP has been endowed with declarative semantics where processes are interpreted as formulas in a given logic. This allows for the use of logical machinery to reason about the behavior of programs and to prove properties of them. Nevertheless, the logical characterization of CCP programs exhibits normally a weak level of adequacy since proofs in the logical system may not correspond directly to traces of the program. In this paper, we study different encodings from CCP into intuitionistic linear logic (ILL) and we compare the level of adequacy attained in each. By relying on a focusing discipline, we show that it is possible to give a logical characterization to CCP with the highest level of adequacy. Moreover, we show how to characterize maximal-parallelism semantics for CCP by relying on a multi-focusing discipline for ILL. These results, besides giving proof techniques for CCP, entail (safe) optimizations for the execution of CCP programs. Finally, we show how to interpret CCP procedure calls as fixed points in ILL, thus opening the possibility of reasoning by induction about properties of CCP programs