A carregar...
Projeto de investigação
LARGE-SCALE INFORMATICS SYSTEMS LABORATORY
Financiador
Autores
Publicações
The Russell-Prawitz embedding and the atomization of universal instantiation
Publication . Espírito Santo, José; Ferreira, Gilda
Given the recent interest in the fragment of system F where universal instantiation
is restricted to atomic formulas, a fragment nowadays named system Fat, we
study directly in system F new conversions whose purpose is to enforce that restriction.
We show some benefits of these new atomization conversions: (1) They
help achieving strict simulation of proof reduction by means of the Russell-Prawitz
embedding of IPC into system F; (2) They are not stronger than a certain “dinaturality”
conversion known to generate a consistent equality of proofs; (3) They
provide the bridge between the Russell-Prawitz embedding and another translation,
due to the authors, of IPC directly into system Fat; (4) They give means for
explaining why the Russell-Prawitz translation achieves strict simulation whereas
the translation into Fat does not.
A refined interpretation of intuitionistic logic by means of atomic polymorphism
Publication . Espírito Santo, José; Ferreira, Gilda
We 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.
Managing missing data and predictions in short time series
Publication . António, Francisco de Araújo; Cavique, Luís
Sales forecasting in the presence of Missing Data poses significant challenges, particularly for short time series where limited observations amplify the impact of incomplete records. This study analyzes a real-world transactional dataset (2021–2024) to predict quantities and prices for 2025. We classify miss-ingness patterns and mechanisms (MCAR, MAR, MNAR) to inform the selection of imputation strategies. We evaluate techniques including MICE, Mean, KNN, and Linear Regression under simulated missingness rates, with KNN emerging as the most robust for the MAR mechanism. Regarding very short-term series pre-dictions, the naive forecast Max2 (maximum of the last two observed values) out-performed moving averages. The results highlight the importance of mechanism-aware imputation and domain-tailored forecasting in sparse datasets. This work presents a practical framework for businesses to effectively utilize incomplete sales data.
Unidades organizacionais
Descrição
Palavras-chave
Contribuidores
Financiadores
Entidade financiadora
Fundação para a Ciência e a Tecnologia
Programa de financiamento
6817 - DCRRNI ID
Número da atribuição
UID/CEC/00408/2019