We present an automated lemma generation method for equational, inductive theorem proving based on the term rewriting induction of Reddy and Aoto as well as the divergence critic framework of Walsh. The method effectively works by using the divergence-detection technique to locate differences in diverging sequences, and generates potential lemmas automatically by analyzing these differences. We have incorporated this method in the multi-context inductive theorem prover of Sato and Kurihara to overcome the strategic problems resulting from the unsoundness of the method. The experimental results show that our method is effective especially for some problems diverging with complex differences (i.e., parallel and nested differences).

Pre-trained CNNs on ImageNet have been widely used in object tracking for feature extraction. However, due to the domain mismatch between image classification and object tracking, the submergence of the target-specific features by noise largely decreases the expression ability of the convolutional features, resulting in an inefficient tracking. In this paper, we propose a robust tracking algorithm with low-dimensional target-specific feature extraction. First, a novel cascaded PCA module is proposed to have an explicit extraction of the low-dimensional target-specific features, which makes the new appearance model more effective and efficient. Next, a fast particle filter process is raised to further accelerate the whole tracking pipeline by sharing convolutional computation with a ROI-Align layer. Moreover, a classification-score guided scheme is used to update the appearance model for adapting to target variations while at the same time avoiding the model drift that caused by the object occlusion. Experimental results on OTB100 and Temple Color128 show that, the proposed algorithm has achieved a superior performance among real-time trackers. Besides, our algorithm is competitive with the state-of-the-art trackers in precision while runs at a real-time speed.

With multiple overlapped piconets, the IEEE 802.15.3 Medium Access Control (MAC) protocol uses a Parent/Child (P/C) or Parent/Neighbor (P/N) configuration to avoid inter-piconet interference. However, the throughput of a P/N or P/C configuration cannot exceed that of a single piconet. In the present paper we propose an efficient means of managing multiple piconets to cooperate with a Multi-Carrier Code Division Multiple Access (MC-CDMA) based UWB system. The proposed management approach uses an Intermediate Device (IDEV) to connect Piconet Coordinators (PNCs). A senior PNC adaptively arranges two simultaneous data transmission links with the proposed spreading matrices in each Channel Time Allocation (CTA) instead of a P/C or P/N configuration, which supports only a single link in each CTA. Simulation results demonstrate the proposed scheme can achieve a higher throughput with an acceptable compromise of link success probability in multiple overlapped piconets.

Restoration is an important area in improving the visual quality, and lays the foundation for accurate object detection or terrain classification in image analysis. In this paper, we introduce Beta process priors into hierarchical sparse Bayesian learning for recovering underlying degraded hyperspectral images (HSI), including suppressing the various noises and inferring the missing data. The proposed method decomposes the HSI into the weighted summation of the dictionary elements, Gaussian noise term and sparse noise term. With these, the latent information and the noise characteristics of HSI can be well learned and represented. Solved by Gibbs sampler, the underlying dictionary and the noise can be efficiently predicted with no tuning of any parameters. The performance of the proposed method is compared with state-of-the-art ones and validated on two hyperspectral datasets, which are contaminated with the Gaussian noises, impulse noises, stripes and dead pixel lines, or with a large number of data missing uniformly at random. The visual and quantitative results demonstrate the superiority of the proposed method.

We conduct, in accordance with IEC 61000-4-2, an electrostatic discharge (ESD) test for a small size battery-operated control circuit board in a myoelectric artificial hand system to investigate the influence of the induced noises by indirect ESDs from an ESD generator to a horizontal coupling plane (HCP) and a vertical coupling plane (VCP). A photo-coupler is set between the small size control board and a motor control circuit to suppress noise in the pulse width modulation (PWM) signals. Two types of ESD noise are observed at the output pins of PWM signals. One type is the ESD noise itself (called Type A) and the other one is the ESD noise superimposed over the PWM pulses (Type B). No matter which polarity the charge voltages of the ESD generator have, both types can be observed and the Type A is dominant in the output pulses. Moreover, the ESD interference in the HCP case is found to be stronger than that in the VCP case usually. In the PWM signals observed at the photo-coupler output, on the other hand, Type A noises tend to increase for positive polarity and decrease for negative polarity, while Type B noises tend to increase at -8kV test level in the HCP case. These results suggest that the photo-coupler does not work well for ESD noise suppression. One of the reasons has been demonstrated to be due to the driving capability of the photo-coupler, and other one is due to the presence of a parasitic capacitance between the input and output of the photo-coupler. The parasitic capacitance can yield a capacitive coupling so that high-frequency ESD noises pass through the photo-coupler.