Abstract
Green energy has become a media issue due to climate changes, and consequently, the population has become more aware of pollution. Wind farms are an essential energy production alternative to fossil energy. The incentive to produce wind energy was a government policy some decades ago to decrease carbon emissions. In recent decades, wind farms were formed by a substation and a couple of turbines. Nowadays, wind farms are designed with hundreds of turbines requiring more than one substation. This paper formulates an integer linear programming model to design wind farms' cable layout with several turbines. The proposed model obtains the optimal solution considering different cable types, infrastructure costs, and energy losses. An additional constraint was considered to limit the number of cables that cross a walkway, i.e., the number of connections between a set of wind turbines and the remaining wind farm. Furthermore, considering a discrete set of possible turbine locations, the model allows identifying those that should be present in the optimal solution, thereby addressing the optimal location of the substation(s) in the wind farm. The paper illustrates solutions and the associated costs of two wind farms, with up to 102 turbines and three substations in the optimal solution, selected among sixteen possible places. The optimal solutions are obtained in a short time.

Abstract
This paper presents a novel iterative three-level optimization framework for the optimal resilient operational scheduling of active multi-carrier energy generation and distribution systems. The main contribution of this paper is that the proposed framework simulates the day-ahead and real-time pre-event preventive and post-event corrective actions for external shocks and explores the effectiveness of risk-averse operational strategies on the system's costs. The solution methodology is another contribution of this paper that finds the optimal scheduling of distributed energy resources and switching of electrical switches and district heating and cooling control valves. At the first stage, the optimal day-ahead scheduling of distributed energy resources and the initial value of the risk control parameter are determined using robust optimization. At the second stage, the optimal realtime market scheduling of distributed energy resources is performed. Finally, at the third stage, different extreme shock scenarios are considered, the effectiveness of corrective actions are investigated, and the value of risk control parameter is modified. The proposed method was successfully applied to the modified 123-bus test system and 600 scenarios of external shocks were considered. The proposed process successfully reduced the expected cost of the. 123-bus system by about 74.59% for the worst-case external shock. Further, the algorithm reduced the aggregated expected values of operational and interruption costs by about 57.73% for all of the 600 cases of the considered external shocks.

Abstract
Multiple traveling salesman problem (mTSP) is a variant of the famous and standard traveling salesman problem, an NP-hard problem in combinatorial optimization. This kind of problem can be solved using exact methods but usually results in high exponential computational complexities. Heuristics and metaheuristics are required to overcome this shortcoming. This study proposes a hybrid method based on the Genetic Algorithm, Ant Colony Optimization, and 2-opt to improve the solution. Computational results with some benchmark instances are provided and compared with other published studies. In three instances, the proposed technique provides better results than the best-known solutions reported in the literature.

Abstract
AbstractIn this study, the geochemistry and mineralogy of regoliths formed on Fogo Island (Cape Verde), a polygenic stratovolcano built during the Quaternary, are used to assess the geomorphological factors that control the early stages of basalt weathering. Fogo Island soils are mainly derived from relatively homogenous silica-undersaturated basaltic rocks. However, a discernible exotic component is recognised in areas most exposed to prevailing winds by ratios on non-mobile elements that are hosted in different amounts by basaltic rocks (e.g., Th, Sc and Ti). Weathering extent is evidenced by a relative depletion in mobile elements (e.g., Na, Ca, Mg) and an enrichment in non-mobile elements (e.g., Ti, Fe, Sc, Al), the decomposition of the most labile minerals (olivines), and the enrichment in secondary components (phyllosilicates and some Fe-oxides, such as hematite-goethite), along with quartz supplied from non-volcanic areas. It depends on bedrock age and type (pyroclastic deposits vs. lava-flows). In particular, soils covering older volcanic units tend to be more affected by chemical alteration than those overlying younger units. In addition, more intense weathering is observed in locations characterised by a combination of moderate elevation, slopes with low gradient and relatively high rainfall. The present investigation shows that even in low humidity environments recently formed basalt are affected by weathering, with the extent of chemical decomposition being mainly determined by the age of surface exposure and local orographic/climatic features.

Abstract
Online incremental models for recommendation are nowadays pervasive in both the industry and the academia. However, there is not yet a standard evaluation methodology for the algorithms that maintain such models. Moreover, online evaluation methodologies available in the literature generally fall short on the statistical validation of results, since this validation is not trivially applicable to stream-based algorithms. We propose a k-fold validation framework for the pairwise comparison of recommendation algorithms that learn from user feedback streams, using prequential evaluation. Our proposal enables continuous statistical testing on adaptive-size sliding windows over the outcome of the prequential process, allowing practitioners and researchers to make decisions in real time based on solid statistical evidence. We present a set of experiments to gain insights on the sensitivity and robustness of two statistical tests-McNemar's and Wilcoxon signed rank-in a streaming data environment. Our results show that besides allowing a real-time, fine-grained online assessment, the online versions of the statistical tests are at least as robust as the batch versions, and definitely more robust than a simple prequential single-fold approach.

Abstract
MATLAB is a software based analysis environment that supports a high-level programing language and is widely used to model and analyze systems in various domains of engineering and sciences. Traditionally, the analysis of MATLAB models is done using simulation and debugging/testing frameworks. These methods provide limited coverage due to their inherent incompleteness. Formal verification can overcome these limitations, but developing the formal models of the underlying MATLAB models is a very challenging and time-consuming task, especially in the case of higher-order-logic models. To facilitate this process, we present a library of higher-order-logic functions corresponding to the commonly used matrix functions of MATLAB as well as a translator that allows automatic conversion of MATLAB models to higher-order logic. The formal models can then be formally verified in an interactive theorem prover. For illustrating the usefulness of the proposed library and approach, we present the formal analysis of a Finite Impulse Response (FIR) filter, which is quite commonly used in digital signal processing applications, within the sound core of the HOL Light theorem prover.