Abstract

Abstract
This work describes a formalization effort, using the Coq proof assistant, of fundamental results related to the classical theory of context-free grammars and languages. These include closure properties (union, concatenation and Kleene star), grammar simplification (elimination of useless symbols, inaccessible symbols, empty rules and unit rules), the existence of a Chomsky Normal Form for context-free grammars and the Pumping Lemma for context-free languages. The result is an important set of libraries covering the main results of context-free language theory, with more than 500 lemmas and theorems fully proved and checked. This is probably the most comprehensive formalization of the classical context-free language theory in the Coq proof assistant done to the present date, and includes the important result that is the formalization of the Pumping Lemma for context-free languages.

Abstract
In this paper we assess the influence of the conductivity of the medium on the radiation characteristics and input impedance of a loop antenna designed for underwater communications. The initial study is based on simulation of the antenna characteristics using FEKO electromagnetic (EM) software. Additionally, an equivalent circuit model of the antenna is also obtained and simulation of the input impedance on ADS software shows good agreement with the EM simulator. It is found that the radiation pattern, of the loop antenna changes significantly with the conductivity of the medium, from freshwater to seawater. The loop antennas were built with baluns and tested in freshwater, where the insertion loss between two identical antennas and the radiation pattern of one of them were also measured. The results show good agreement with the simulations.

Abstract
From social networks to health and fitness, everyday a lot of mobile devices applications (apps) are being developed. The variety and availability is such that people start to think that indeed "there's an app for everything". Many of these apps address either problems or characteristics that affect older people and that are related with the ageing process (e.g. memory and visual aids apps). They can effectively help people and are under constant evolution. However, the lack of knowledge about these available technological aids can undermine its dissemination and consequently the help that people really receive, especially those who need it the most: older people. As such, a methodological search for available aid apps was made both in Google Play and in iTunes: 536 were selected, their classification analysed and the kind of help that they provide identified. It was noted that either in Google Play or in iTunes the apps' categories are similar. Furthermore, it is not easily perceived what the type of help that each app can provide is and how is it provided. Hence, based on the results from the aforementioned methodological search, this paper proposes a new scalable tree-based classification methodology for aid apps, which is considered more suited to perceive what the available aid apps for mobile devices are. The existing apps were then characterized based on the proposed classification, to determine what the main aid that they provide is. (C) 2016 The Authors. Published by Elsevier BAT.

Abstract
This paper presents two new approaches to solve the reconfiguration problem of electrical distribution systems (EDSs) with variable demands, using the CLONALG and the SGACB algorithms. The CLONALG is a combinatorial optimization technique inspired by biological immune systems, which aims at reproducing the main properties and functions of the system. The SGACB is an optimization algorithm inspired by natural selection and the evolution of species. The reconfiguration problem with variable demands is a complex combinatorial problem that aims at identifying the best radial topology for an EDS, while satisfying all technical constraints at every demand level and minimizing the cost of energy losses in a given operation period. Both algorithms were implemented in C++ and test systems with 33, 84, and 136 nodes, as well as a real system with 417 nodes, in order to validate the proposed methods. The obtained results were compared with results available in the literature in order to verify the efficiency of the proposed approaches.

Abstract