Abstract
Kleene algebra with tests (KAT) was introduced as an algebraic structure to model and reason about classic imperative programs, i.e. sequences of discrete transitions guarded by Boolean tests. This paper introduces two generalisations of this structure able to express programs as weighted transitions and tests with outcomes in non necessarily bivalent truth spaces: graded Kleene algebra with tests (GKAT) and a variant where tests are also idempotent (I-GKAT). In this context, and in analogy to Kozen's encoding of Propositional Hoare Logic (PHL) in KAT we discuss the encoding of a graded PHL in I-GKAT and of its while-free fragment in GKAT. Moreover, to establish semantics for these structures four new algebras are defined: FSET(T), FREL(K,T) and FLANG(K,T) over complete residuated lattices K and T, and M (n, A) over a GKAT or I-GKAT A. As a final exercise, the paper discusses some program equivalence proofs in a graded context.

Abstract
Though Motor Imagery (MI) stroke rehabilitation effectively promotes neural reorganization, current therapeutic methods are immeasurable and their repetitiveness can be demotivating. In this work, a real-time electroencephalogram (EEG) based MI-BCI (Brain Computer Interface) system with a virtual reality (VR) game as a motivational feedback has been developed for stroke rehabilitation. If the subject successfully hits one of the targets, it explodes and thus providing feedback on a successfully imagined and virtually executed movement of hands or feet. Novel classification algorithms with deep learning (DL) and convolutional neural network (CNN) architecture with a unique trial onset detection technique was used. Our classifiers performed better than the previous architectures on datasets from PhysioNet offline database. It provided fine classification in the real-time game setting using a 0.5 second 16 channel input for the CNN architectures. Ten participants reported the training to be interesting, fun and immersive. "It is a bit weird, because it feels like it would be my hands", was one of the comments from a test person. The VR system induced a slight discomfort and a moderate effort for MI activations was reported. We conclude that MI-BCI-VR systems with classifiers based on DL for real-time game applications should be considered for motivating MI stroke rehabilitation. © 2019 Association for Computing Machinery.

Abstract
Vine culture is influenced by many factors, such as the weather, soil or topography, which are triggers to phytosanitary issues. Among them are some diseases, that are responsible for major economic losses that can, however, be managed with timely interventions in the field, viable of leading to effective results by preventing damage propagation. While not all symptoms might present a visible evidence, hyperspectral sensors can tackle this aspect with their ability for measuring hundreds of continuously sparse bands that range beyond the eye-perceptible spectrum. Having such research line in mind in this work, a hyperspectral sensor was applied to analyse the spectral status of vine leaves samples, collected in three chronologically distinct campaigns, while costly and destructive laboratory methods were used to track Flavescence Dorée (FD) in the same samples, for a ground truth information. Regarding data processing, machine learning approaches were used, in which several classifiers were selected to detect FD in vine leaves hyperspectral images. The goal was to evaluate and find most suitable classifier for this task. © 2019 International Society for Photogrammetry and Remote Sensing.

Abstract
Dynamic logic is a powerful framework for reasoning about imperative programs. This paper extends previous work [9] on the systematic generation of dynamic logics from the propositional to the equational case, to capture ‘full-fledged’ imperative programs. The generation process is parametric on a structure specifying a notion of ‘weight’ assigned to programs. The paper introduces also a notion of bisimilarity on models of the generated logics, which is shown to entail modal equivalence with respect to the latter. © 2019, Springer Nature Switzerland AG.

Abstract
This work proposes a new design for the supporting data structures used to implement multithreaded tabling in Prolog systems. Tabling is an implementation technique that improves the expressiveness of traditional Prolog systems in dealing with recursion and redundant computations. Mode-directed tabling is an extension to the tabling technique that supports the definition of alternative criteria for specifying how answers are aggregated, thus being very suitable for problems where the goal is to dynamically calculate optimal or selective answers. In this work, we leverage the intrinsic potential that mode-directed tabling has to express dynamic programming problems by creating a new design that improves the representation of multi-dimensional arrays in the context of multithreaded tabling. To do so, we introduce a new mode for indexing arguments in mode-directed tabled evaluations, named dim, where each dim argument features a uni-dimensional lock-free array. Experimental results using well-known dynamic programming problems on a 32-core machine show that the new design introduces less overheads and clearly improves the execution time for sequential and multithreaded tabled evaluations.

Abstract
This chapter presents how multimodal narratives were employed as a self-reflection tool within an online professional development program for in-service teacher training at Universidade Aberta, Portugal during two editions of a pedagogic practice course. The chapter includes the aspects that raised issues and those that trainees performed correctly. This is done in three stages: beforehand, upon initial contact with multimodal narratives, and after providing feedback to trainees. The most relevant issues were in aspects directly required to enrich the narrative. Aspects related to multimodal narrative structure and features were completed successfully. It is recommended that future attempts to employ multimodal narratives in this context adapt learning resources and pedagogic support practices by employing formative feedback and continual support during the trainees' process of exploring and exploiting multimodal narratives. © 2019, IGI Global.