V.M. Glushkov and automated theorem proving in Ukraine: evidence algorithm evidence algorithm and SAD systems

Fifty years ago, in 1970, Academician V.M. Glushkov published a paper, in which he, along with a discussion of some problems of artificial intelligence, formulated a research program called Evidence Algorithm (EA) describing his vision of the problem of a computer support of human activity in looking for a proof of a particular theorem. V.M. Glushkov proposed to focus attention on the construction of an automated theorem-proving system performing simultaneous investigations in: creating formal natural languages for writing mathematical texts in a form accustomed to a human, constructing a procedure for a proof search based on the evolutionary developing of the machine notion of an evidence of a computer-made proof step, using the knowledge gained by the system during its operation and providing a user with the opportunity to assist to the system in its proof search process. Since the inception of EA, two serious attempts have been made to implement this program. The first led to the emergence in 1978 of a Russian-language automated theorem proving and the second led to the appearance in 2002 of its English-language modification named System for Automated Deduction (SAD). And if the development and trial operation of the first system were discontinued in 1992 after the output from service of the ES-line computers, on which it was realized, the SAD system, being placed on the website “nevidal.org”, is now still available in online mode. That is, at the current time, it is possible to carry out different experiments with the SAD system and to solve various problems that require rigorous mathematical reasoning. This work is devoted to a chronological description of studies on the implementation of the EA program for the entire period of its existence and to the highlighting of peculiarities of both the systems, as well as of their common features and distinguishes. Some possible ways of the further development of the SAD system are given.

An Information Fusion Model Based on Dempster–Shafer Evidence Theory for Equipment Diagnosis

An abnormal operating effect can be caused by different faults, and a fault can cause different abnormal effects. An information fusion model, with hybrid-type fusion frame, is built in this paper, so as to solve this problem. This model consists of data layer, feature layer and decision layer, based on an improved Dempster–Shafer (D-S) evidence algorithm. After the data preprocessing based on event reasoning in data layer and feature layer, the information will be fused based on the new algorithm in decision layer. Application of this information fusion model in fault diagnosis is beneficial in two aspects, diagnostic applicability and diagnostic accuracy. Additionally, this model can overcome the uncertainty of information and equipment to increase diagnostic accuracy. Two case studies are implemented by this information fusion model to evaluate it. In the first case, fault probabilities calculated by different methods are adopted as inputs to diagnose a fault, which is quite different to be detected based on the information from a single analytical system. The second case is about sensor fault diagnosis. Fault signals are planted into the measured parameters for the diagnostic system, to test the ability to consider the uncertainty of measured parameters. The case study result shows that the model can identify the fault more effectively and accurately. Meanwhile, it has good expansibility, which may be used in more fields.

Image Tampering with Evidence Algorithm Based on Copy and Paste

Authenticity, integrity and authentication primitive technology for digital image content case of digital image forensics, as one branch of information security technology, is not pre-embedded image watermarks to forensic identification. In this paper, a common digital image tampering copy and paste operations have been studied and proposed detection method for this operation to improve the robustness of the algorithm.