Matemática e Estatística | Artigos em revistas internacionais / Papers in international journals
Permanent URI for this collection
Browse
Browsing Matemática e Estatística | Artigos em revistas internacionais / Papers in international journals by Sustainable Development Goals (SDG) "04:Educação de Qualidade"
Now showing 1 - 7 of 7
Results Per Page
Sort Options
- Atomic polymorphismPublication . Ferreira, Fernando; Ferreira, GildaIt has been known for six years that the restriction of Girard’s polymorphic system F to atomic universal instantiations interprets the full fragment of the intuitionistic propositional calculus. We firstly observe that Tait’s method of “convertibility” applies quite naturally to the proof of strong normalization of the restricted Girard system. We then show that each β-reduction step of the full intuitionistic propositional calculus translates into one or more βη-reduction steps in the restricted Girard system. As a consequence, we obtain a novel and perspicuous proof of the strong normalization property for the full intuitionistic propositional calculus. It is noticed that this novel proof bestows a crucial role to η-conversions.
- Atomic polymorphism and the existence propertyPublication . Ferreira, GildaWe present a purely proof-theoretic proof of the existence property for the full intuitionistic first-order predicate calculus, via natural deduction, in which commuting conversions are not needed. Such proof illustrates the potential of an atomic polymorphic system with only three generators of formulas – conditional and first and second-order universal quantifiers – as a tool for proof-theoretical studies.
- Herbrandized modified realizabilityPublication . Ferreira, Gilda; Firmino, PauloRealizability notions in mathematical logic have a long history, which can be tracedback to the work of Stephen Kleene in the 1940s, aimed at exploring the foundations ofintuitionistic logic. Kleene’s initial realizability laid the ground for more sophisticatednotions such as Kreisel’s modified realizability and various modern approaches. Inthis context, our work aligns with the lineage of realizability strategies that emphasizethe accumulation, rather than the propagation of precise witnesses. In this paper, weintroduce a new notion of realizability, namely herbrandized modified realizability.This novel form of (cumulative) realizability, presented within the framework of semi-intuitionistic logic is based on a recently developed star combinatory calculus, whichenables the gathering of witnesses into nonempty finite sets. We also show that theprevious analysis can be extended from logic to (Heyting) arithmetic.
- A new R-function to estimate the PDF of the product of two uncorrelated normal variablesPublication . Seijas-Macias, J. Antonio; Oliveira, Amilcar; Oliveira, TeresaThis paper analyses the implementation of a procedure using the software R to calculate the Probability Density Function (PDF) of the product of two uncorrelated Normally Distributed Random Variables. The problem of estimating the distribution of the product of two random variables has been solved for some particular cases, but there is no unique expression for all possible situations. In our study, we chose Rohatgi’s theorem as a basis for approximating the product of two uncorrelated Normally Distributed Random Variables. The numerical approximation of the product PDF was calculated using a function that we implemented in R. Several numerical examples show that the approximations obtained in R fit the theoretical values of the product distributions. The results obtained with our R function are very positive when we compare them with the Monte Carlo Simulation of the product of the two variables.
- A refined interpretation of intuitionistic logic by means of atomic polymorphismPublication . Espírito Santo, José; Ferreira, GildaWe study an alternative embedding of IPC into atomic system F whose translation of proofs is based, not on instantiation overflow, but instead on the admissibility of the elimination rules for disjunction and absurdity (where these connectives are defined according to the Russell- Prawitz translation). As compared to the embedding based on instantiation overflow, the alternative embedding works equally well at the levels of provability and preservation of proof identity, but it produces shorter derivations and shorter simulations of reduction sequences. Lambda-terms are employed in the technical development so that the algorithmic content is made explicit, both for the alternative and the original embeddings. The investigation of preservation of proof-reduction steps by the alternative embedding enables the analysis of generation of “administrative” redexes. These are the key, on the one hand, to understand the difference between the two embeddings; on the other hand, to understand whether the final word on the embedding of IPC into atomic system F has been said.
- The computational content of atomic polymorphismPublication . Ferreira, Gilda; Vasconcelos, Vasco TWe show that the number-theoretic functions de nable in the atomic polymorphic system (Fat) are exactly the extended polynomials. Two proofs of the above result are presented: one reducing the functions' de n- ability problem in Fat to de nability in the simply typed lambda-calculus and other directly adapting Helmut Schwichtenberg's strategy for de nability in the simply typed lambda-calculus to the atomic polymorphic setting. The uniformity granted in the polymorphic system, when compared with the simply typed lambda-calculus, is emphasized.
- The Mixed CUSUM-EWMA (MCE) control chart as a new alternative in the monitoring of a manufacturing processPublication . Oliveira, Amilcar; Oliveira, Teresa A.; Paladini, Edson Pacheco; Walter, Olga Maria Formigoni Carvalho; Henning, Elisa; Konrath, Andréa Cristina; Alves, Custodio da CunhaGoal: The objective is to conclude, based on a comparative study, if there is a significant difference in sensitivity between the application of MCE and the individual application of the CUSUM or EWMA chart, i.e., greater sensitivity particularly for cases of lesser magnitude of change. Design/Methodology/Approach: These are an applied research and statistical techniques such as statistical control charts are used for monitoring variability. Results: The results show that the MCE chart signals a process out of statistical control, while individual EWMA and CUSUM charts does not detect any situation out of statistical control for the data analyzed. Limitations: This article is dedicated to measurable variables and individual analysis of quality characteristics, without investing in attribute variables. The MCE chart was applied to items that are essential to the productive process development being analysed. Practical Implications: The practical implications of this study can contribute to: the correct choice of more sensitive control charts to detect mainly small changes in the location (mean) of processes; provide clear and accurate information about the fundamental procedures for the implementation of statistical quality control; and encourage the use of this quality improvement tool. Originality/Value: The MCE control chart is a great differential for the improvement of the quality process of the studied company because it goes beyond what CUSUM and EWMA control charts can identify in terms of variability.