Deciding Kleene Algebra Terms Equivalence in Coq

This paper presents a mechanically verified implementation of an algorithm for deciding the equivalence of Kleene algebra terms within the Coq proof assistant. The algorithm decides equivalence of two given regular expressions through an iterated process of testing the equivalence of their partial derivatives and does not require the construction of the corresponding automata. Recent theoretical and experimental research provides evidence that this method is, on average, more efficient than the classical methods based on automata. We present some performance tests, comparisons with similar approaches, and also introduce a generalization of the algorithm to decide the equivalence of terms of Kleene algebra with tests. The motivation for the work presented in this paper is that of using the libraries developed as trusted frameworks for carrying out certified program verification.

The Interpretation of Verbal Probability Expressions Used in the IAS/IFRS: the auditors Rrgistered with the portuguese securities market commission

One of the main arguments in favour of the adoption and convergence with the international accounting standards published by the IASB (i.e. IAS/IFRS) is that these will allow comparability of financial reporting across countries. However, because these standards use verbal probability expressions (v.g. “probable”) when establishing the recognition and disclosure criteria for accounting elements, they require professional accountants to interpret and classify the probability of an outcome or event taking into account those terms and expressions and to best decide in terms of financial reporting. This paper reports part of a research we carried out on the interpretation of “in context” verbal probability expressions used in the IAS/IFRS by the auditors registered with the Portuguese Securities Market Commission, the Comissão do Mercado de Valores Mobiliários (CMVM). Our results provide support for the hypothesis that culture affects the CMVM registered auditors’ interpretation of verbal probability expressions through its influence on the accounting value (or attitude) of conservatism. Our results also suggest that there are significant differences in their interpretation of the term “probable”, which is consistent with literature in general. Since “probable” is the most frequent verbal probability expression used in the IAS/IFRS, this may have a negative impact on financial statements comparability.

A simplified four-branch model for the analytical study of the out-of-plane performance of regular stone URM walls

During the last years, several studies have been made aiming to assess the out-of-plane seismic response of unreinforced stone masonry structures. This fact led to the development of a wide variety of models and approaches, ranging from simple kinematic based analytical models up to complex numerical simulations. Nevertheless, for the sake of simplicity, the out-of-plane seismic response of a masonry wall pier may be obtained by means of a simple single-degree-of-freedom system while still providing good results. In fact, despite the assumptions associated with such a simple formulation, it is also true that the epistemic uncertainty inherent with the selection of appropriate input parameters in more complex models may render them truly ineffective. In this framework, this paper focuses on the study of the out-of-plane bending of unreinforced stone masonry walls (cantilevers) by proposing a simplified analytical approach based on the construction of a linearized four-branch model, which is used to characterize the linear and nonlinear response of such structural elements through an overturning moment-rotation relationship. The formulation of the four-branch model is presented and described in detail and the meaningful parameters used for its construction are obtained from a set of experimental laboratory tests performed on six full-scale unreinforced regular sacco stone masonry specimens. Moreover, a parametric analysis aiming to evaluate the effect of these parameters’ variation on the final configuration of the model is presented and critically discussed. Finally, the results obtained from the application of the developed four-branch model on real unreinforced regular sacco stone masonry walls are thoroughly analysed and the main conclusions obtained from its application are summarized.

Experimental characterization of the out-of-plane performance of regular stone masonry walls, including test setups and axial load influence

Stone masonry is one of the oldest and most worldwide used building techniques. Nevertheless, the structural response of masonry structures is complex and the effective knowledge about their mechanical behaviour is still limited. This fact is particularly notorious when dealing with the description of their out-of-plane behaviour under horizontal loadings, as is the case of the earthquake action. In this context, this paper describes an experimental program, conducted in laboratory environment, aiming at characterizing the out-of-plane behaviour of traditional unreinforced stone masonry walls. In the scope of this campaign, six full-scale sacco stone masonry specimens were fully characterised regarding their most important mechanic, geometric and dynamic features and were tested resorting to two different loading techniques under three distinct vertical pre-compression states; three of the specimens were subjected to an out-of-plane surface load by means of a system of airbags and the remaining were subjected to an out-of-plane horizontal line-load at the top. From the experiments it was possible to observe that both test setups were able to globally mobilize the out-of-plane response of the walls, which presented substantial displacement capacity, with ratios of ultimate displacement to the wall thickness ranging between 26 and 45 %, as well as good energy dissipation capacity. Finally, very interesting results were also obtained from a simple analytical model used herein to compute a set of experimental-based ratios, namely between the maximum stability displacement and the wall thickness for which a mean value of about 60 % was found.

Que alternativa ao currículo regular no ensino básico?

Encaramos o currículo como um projeto em constante transformação, que tendo por referência o currículo nacional, é adequado ao seu públicoalvo, os alunos. No contexto de cada comunidade onde a escola está inserida, a definição das ofertas educativas/curriculares assume maior pertinência, podendo contemplar componentes locais e regionais do currículo, valorizando as caraterísticas de cada região e, sobretudo, engrandecer os talentos dos alunos, de acordo com as suas especificidades individuais. A reflexão, realizada em torno das dificuldades que muitos alunos têm em realizar as aprendizagens previstas no currículo oficial, deu origem a uma questão central: Que alternativa ao currículo regular no ensino básico? Na procura de respostas à questão, abordamos o nascimento da escola e conceitualização de currículo, a evolução da formação para o mundo do trabalho, a diversificação curricular e a autonomia da escola. O estudo empírico seguiu uma metodologia quantitativa e qualitativa, através de um estudo de caso e centrou-se: na análise documental do Projeto Educativo do Agrupamento; inquérito por questionário aos alunos do terceiro ciclo do ensino básico, regular e cursos vocacionais; inquérito por entrevistas semiestruturadas ao Presidente do Conselho Geral do Agrupamento, Diretora do Agrupamento, Coordenadoras de Departamento, Coordenador dos Cursos Vocacionais e representante no Conselho Pedagógico dos Serviços de Psicologia e Orientação. Expomos as conclusões da investigação através da triangulação dos dados obtidos com os instrumentos de recolha. Como resposta à questão inicial, apresentamos uma proposta alternativa ao currículo regular do ensino básico, que procura diversificar a oferta.