Convolutional Neural Network-Based Identity Recognition Using ECG atDifferent Water Temperatures During Bathing

This study proposes a convolutional neural network(CNN)-based identity recognition scheme using electrocardiogram(ECG)at different water temperatures(WTs)during bathing,aiming to explore the impact of ECG length on the recognition rate.ECG data was collected using non-contact electrodes at five different WTs during bathing.Ten young student subjects(seven men and three women)participated in data collection.Three ECG recordings were collected at each preset bathtub WT for each subject.Each recording is 18 min long,with a sampling rate of 200 Hz.In total,150 ECG recordings and 150 WT recordings were collected.The R peaks were detected based on the processed ECG(baseline wandering eliminated,50-Hz hum removed,ECG smoothing and ECG normalization)and the QRS complex waves were segmented.These segmented waves were then transformed into binary images,which served as the datasets.For each subject,the training,validation,and test data were taken from the first,second,and third ECG recordings,respectively.The number of training and validation images was 84297 and 83734,respectively.In the test stage,the preliminary classification results were obtained using the trained CNN model,and the finer classification results were determined using the majority vote method based on the preliminary results.The validation rate was 98.71%.The recognition rates were 95.00%and 98.00%when the number of test heartbeats was 7 and 17,respectively,for each subject.

An Improvement of Herbrand's Theorem and Its Application to Model Generation Theorem Proving

This paper presents an improvement of Herbrand＇s theorem. We propose a method for specifying a subuniverse of the Herbrand universe of a clause set S for each argument of predicate symbols and function symbols in S. We prove that a clause set S is unsatisfiable if and only if there is a finite unsatisfiable set of ground instances of clauses of S that are derived by only instantiating each variable, which appears as an argument of predicate symbols or function symbols, in S over its corresponding argument＇s sub-universe of the Herbrand universe of S. Because such sub-universes are usually smaller （sometimes considerably） than the Herbrand universe of S, the number of ground instances may decrease considerably in many cases. We present an algorithm for automatically deriving the sub-universes for arguments in a given clause set, and show the correctness of our improvement. Moreover, we introduce an application of our approach to model generation theorem proving for non-range-restricted problems, show the range-restriction transformation algorithm based on our improvement and provide examples on benchmark problems to demonstrate the power of our approach.