Abstract
Despite great advances in computer-assisted proof systems, writing formal proofs using a traditional computer is still challenging due to mouse-and-keyboard interaction. This leads to scientists often resorting to pen and paper to write their proofs. However, when handwriting a proof, there is no formal guarantee that the proof is correct. In this paper we address this issue and present the initial steps towards a system that allows users to handwrite proofs using a pen-based device and that communicates with an external theorem prover to support the users throughout the proof writing process. We focus on calculational proofs, whereby a theorem is proved by a chain of formulae, each transformed in some way into the next. We present the implementation of a proof-of-concept prototype that can formally verify handwritten calculational proofs without the need to learn the specific syntax of theorem provers.

Abstract
Pose invariant object detection and classification plays a critical role in robust image recognition systems and can be applied in a multitude of applications, ranging from simple monitoring to advanced tracking. This paper analyzes the usage of the Bag of Words model for recognizing objects in different scales, orientations and perspective views within cluttered environments. The recognition system relies on image analysis techniques, such as feature detection, description and clustering along with machine learning classifiers. For pinpointing the location of the target object, it is proposed a multiscale sliding window approach followed by a dynamic thresholding segmentation. The recognition system was tested with several configurations of feature detectors, descriptors and classifiers and achieved an accuracy of 87% when recognizing cars from an annotated dataset with 177 training images and 177 testing images. © Springer International Publishing AG 2018.

Abstract
This study presents innovative analysis at the time, frequency and phase domain of the pelvis angular oscillation at transverse (T), sagittal (S) and coronal (C) planes, assessing its coordination during stiff knee gait (SKG) and slow running (SR) comparing it to normal gait (NG). Case study is considered of an adult male 70 kg mass and 1.86 m height. Computer vision is used with 8 Qualysis 100 Hz cameras tracking position of right and left anterior and posterior superior iliac spine (RAsis, LAsis, RPsis, LPsis) including one complete stride during NG, SKG and SR. 3D position coordinates are obtained from 2D image coordinate of multiple camera image using direct linear transformation (DLT). Inverse kinematics is performed using cartesian position data of RAsis, LAsis, RPsis, LPsis and scaled model to subject dimension. The angles, angular velocities and angular accelerations coordination of the pelvis oscillation at T, S, C planes were assessed using linear and cross correlation analysis (LCA, CCA), fast Fourier transform (FFT) and phase space analysis (PSA). Results point for important complementary analysis on entire series of time, frequency and phase analysis of human movement such as the pelvis coordination assessment on different gait modes.

Abstract
Vineyard parcels delimitation is a preliminary but important task to support zoning activities, which can be burdensome and time-consuming when manually performed. In spite of being desirable to overcome such issue, the implementation of a semi-/fully automatic delimitation approach can meet serious development challenges when dealing with vineyards like the ones that prevail in Douro Region (north-east of Portugal), mainly due to the great diversity of parcel/row formats and several factors that can hamper detection as, for example, interrupted rows and inter-row vegetation. Thereby, with the aim of addressing vineyard parcels detection and delimitation in Douro Region, a preliminary method based on segmentation and morphological operations upon high-resolution aerial imagery is proposed. This method was tested in a data set collected from vineyards located at the University of Trás-os-Montes and Alto Douro(Vila Real, Portugal). The presence of some of the previously mentioned challenging conditions - namely interrupted rows and inter-row grassing - in a few parcels contributed to lower the overall detection accuracy, pointing out the need for future improvements. Notwithstanding, encouraging preliminary results were achieved. © 2018 Association for Computing Machinery.

Abstract
Recent years have witnessed an increased interest, by competition agencies, in assessing the competitive effects of partial acquisitions. We propose a generalization of the two most traditional indicators used to screen unilateral anti-competitive effects - the HerfindahlHirschman Index and the Gross Up- ward Price Pressure Index - to partial horizontal acquisition settings. The proposed generalized indicators are endogenously derived under a probabilistic voting model in which the manager of each firm is elected in a shareholder assembly between two potential candidates who seek to obtain utility from an exogenous rent associated with corporate office. The model (i) can cope with settings involving all types of owners and rights: owners that can be internal to the industry (rival firms) and external to the industry; and rights that can capture financial and corporate control interests, can be direct and indirect, can be partial or full, (ii) yields an endogenous measure of the owners ultimate corporate control rights, and (iii) can also be used - in case the potential acquisition is inferred to likely enhance market power - to devise divestiture structural remedies. We also provide an empirical application of the two proposed generalized indicators to several acquisitions in the wet shaving industry, with the objective of providing practitioners with a step-by-step illustration of how to compute them in antitrust cases.

Abstract