Search

The genome of the novel coronavirus (COVID-19) disease was first sequenced in January 2020, approximately a month after its emergence in Wuhan, capital of Hubei province, China. COVID-19 genome sequencing is critical to understanding the virus behavior, its origin, how fast it mutates, and for the development of drugs/vaccines and effective preventive strategies. This paper investigates the use of artificial intelligence techniques to learn interesting information from COVID-19 genome sequences. Sequential pattern mining (SPM) is first applied on a computer-understandable corpus of COVID-19 genome sequences to see if interesting hidden patterns can be found, which reveal frequent patterns of nucleotide bases and their relationships with each other. Second, sequence prediction models are applied to the corpus to evaluate if nucleotide base(s) can be predicted from previous ones. Third, for mutation analysis in genome sequences, an algorithm is designed to find the locations in the genome sequences where the nucleotide bases are changed and to calculate the mutation rate. Obtained results suggest that SPM and mutation analysis techniques can reveal interesting information and patterns in COVID-19 genome sequences to examine the evolution and variations in COVID-19 strains respectively.

Interactive theorem provers (ITPs), also known as proof assistants, allow human users to write and verify formal proofs. The proof development process in ITPs can be a cumbersome and time-consuming activity due to manual user interactions. This makes proof guidance and proof automation the two most desired features for ITPs. In this paper, we first provide two evolutionary and heuristic-based proof searching approaches for the HOL4 proof assistant, where a genetic algorithm (GA) and simulated annealing (SA) is used to search and optimize the proofs in different HOL theories. In both approaches, random proof sequences are first generated from a population of frequently occurring HOL4 proof steps that are discovered with sequential pattern mining. Generated proof sequences are then evolved using GA operators (crossover and mutation) and by applying the annealing process of SA till their fitness match the fitness of the target proof sequences. Experiments were done to compare the performance of SA with that of GA. Results have shown that the two proof searching approaches can be used to efficiently evolve the random sequences to obtain the target sequences. However, these approaches lack the ability to learn the proof process, that is important for the prediction of new proof sequences. For this purpose, we propose to use a deep learning technique known as long short-term memory (LSTM). LSTM is trained on various HOL4 theories for proof learning and prediction. Experimental results suggest that combining evolutionary/heuristic and deep learning techniques with proof assistants can greatly facilitate proof finding/optimization and proof prediction.

Interactive theorem provers (ITPs) are software tools that allow human users to write and verify formal proofs. In recent years, an emerging research area in ITPs is proof mining, which consists of identifying interesting proof patterns that can be used to guide the interactive proof process in ITPs. In previous studies, some data mining techniques, such as frequent pattern mining, have been used to analyze proofs to find frequent proof steps. Though useful, such models ignore the facts that not all proof steps are equally important. To address this issue, this paper proposes a novel proof mining approach based on finding not only frequent patterns but also high utility patterns to find proof steps of high importance (utility). A proof process learning approach is proposed based on high utility itemset mining (HUIM) for the PVS (Prototype Verification System) proof assistant. Proofs in PVS theories are first abstracted to a computer-processable corpus, where each line represents a proof sequence and proof commands in proof sequences are associated with utilities representing their weightage (importance). HUIM techniques are then applied on the corpus to discover frequent proof steps/high utility patterns and their relationships with each other. Experimental results suggest that combining frequent pattern mining techniques, such as sequential pattern mining and high utility itemset mining, with proof assistants, such as PVS, is useful to learn and guide the proof development process.

Disorders of the heart and blood vessels are named cardiovascular disease. 'The heart's proper functionality is of an utmost necessity for the survival of life. The death rate due to heart disease, has been increased rapidly. Cardiovascular illness is believed the deadliest cause of death across the globe. From the facts and figures shared by the WHO (World Health Organization) 17.9 Million human lost their lives due to cardiovascular diseases. This research is carried out for the effective diagnosis of heart disease using the heart disease dataset available on the UCI Machine Repository. Heart disease diagnosis with an optimization algorithm can be fruitful in terms of higher accuracy and sensitivity. Finding an acceptable optimal solution among multiple solutions for a specific problem is known as optimization. Different machine learning algorithms have been applied as Support Machine Vector (SVM), K-Nearest Neighbor (KNN), Naïve Bayes (NB), Artificial Neural Network (ANN), Random Forest (RF), and Gradient Descent Optimization (GDO). Intelligent Cardiovascular Disease Prediction Empowered with Gradient Descent Optimization model produces the optimal results among under consideration classification algorithms. 98.54 % accuracy has been achieved by the GDO based model while performance evaluation it. 99.43% sensitivity (recall) and 97.76% precision have also been recorded. From the prediction results of the system, it's satisfactory to utilize it for cardiovascular disease diagnosis. The proposed system will be helpful for the analysis of cardiovascular disease., Gradient descent: optimization; Prediction model; Cardiovascular disease.

Examining the genome sequences of the novel coronavirus (COVID-19) strains is critical to properly understand this disease and its functionalities. In bioinformatics, alignment-free (AF) sequence analysis methods offer a natural framework to investigate and understand the patterns and inherent properties of biological sequences. Thus, AF methods are used in this paper for the analysis and comparison of COVID-19 genome sequences. First, frequent patterns of nucleotide base(s) in COVID-19 genome sequences are extracted. Second, the similarity/dissimilarity between COVID-19 genome sequences are measured with different AF methods. This allows to compare sequences and evaluate the performance of various distance measures employed in AF methods. Lastly, the phylogeny for the COVID-19 genome sequences are constructed with various AF methods as well as the consensus tree that shows the level of support (agreement) among phylogenetic trees built by various AF methods. Obtained results show that AF methods can be used efficiently for the analysis of COVID-19 genome sequences.

Genetic Algorithms (GAs) are an excellent approach for mining high-utility itemsets (HUIs) as they can discover most of the HUIs in a fraction of the time spent by exact algorithms. A key feature of GAs is crossover operators, which allow individuals in a population to communicate and exchange information with each other. However, the usefulness of crossover operator in the overall progress of GAs for high-utility itemset mining (HUIM) has not been investigated. In this paper, the headless chicken test is used to analyze four GAs for HUIM. In that test, crossover operators in the original GAs for HUIM are first replaced with randomized crossover operators. Then, the performance of original GAs with normal crossover are compared with GAs with random crossover. This allows evaluating the overall usefulness of crossover operators in the progress that GAs make during the search and evolution process. Through this test, we found that one GA for HUIM performed poorly, which indicates the absence of well-defined building blocks and that crossover in that GA was indeed working as a macromutation.

The proof development process in PVS theorem prover is interactive in nature, that is not only laborious but consumes lots of time. For proof searching and optimization in PVS, a heuristic proof searching approach is provided where simulated annealing (SA) is used to search and optimize the proofs for formalized theorems/lemmas in PVS theories. In the proposed approach, random proof sequence is first generated from a population of frequently occurring PVS proof steps that are discovered with sequential pattern mining. Generated proof sequence then goes through the annealing process till its fitness matches with the fitness of the target proof sequence. Moreover, the performance of SA with a genetic algorithm (GA) is compared. Obtained results suggest that evolutionary/heuristic techniques can be combined with proof assistants to efficiently support proofs finding and optimization.

Generally, two topics with vastly different terminology probably indicate different implied concepts. However, these topics themselves might share common references (bibliographic coupling), which suggest the underlying joint concept. Therefore, searching for these joint concepts in different topics would be of scientific interest. Previous studies have measured the similarity between topics based on comparison of the topics' word probability distributions. In contrast, this paper presents an approach for measuring the similarity between topics based on the bibliographic coupling. Besides, the similarity is independent of the topic's word probability distributions generated by a Latent Dirichlet Allocation (LDA) model. The proposed approach was evaluated using its counterpart (intra-topic similarity), baseline topic similarity matrices, and cosine measure. The method was exampled on brain cancer patents. A cross-topic similarity network of eight topics showcases 28 cross-topic pairs to profile which topics were associated with particular topics. Interestingly, some of the 28 combinations may be of scientific interest. For instance, the findings of the top five cross-topic pairs suggest that “growth of cancer cells” and “imbalances in the hormones” have common knowledge sources with the highest similarity value. These two entirely different concepts may suggest some common causative factors within the field. We believe that finding such an association between unrelated innovative inventions across various industries may help public and private research units in planning research direction and serve as a reference for future research.

Proof searching and proof automation are the two most desired properties in interactive theorem provers (ITPs) as they generally require manual user guidance, which can be quite cumbersome. In this paper, we provide an evolutionary proof searching approach for the HOL4 proof assistant, where a genetic algorithm (GA) with different crossover and mutation operators is used to search and optimize the proofs in different HOL theories. Random proof sequences are first generated from a population of frequently occurring HOL4 proof steps that are discovered with sequential pattern mining. Generated proof sequences are then evolved with GA operators (three crossover and two mutation) till their fitness match the fitness of the target proof sequences. Various crossover and mutation operators are used to compare their effect on the performance of GAs in proof searching. Obtained results suggest that integrating GAs with HOL4 allows us to efficiently support proof finding and optimization.

Purpose Twitter users’ generated data, known as tweets, are now not only used for communication and opinion sharing, but they are considered an important source of trendsetting, future prediction, recommendation systems and marketing. Using network features in tweet modeling and applying data mining and deep learning techniques on tweets is gaining more and more interest. Design/methodology/approach In this paper, user interests are discovered from Twitter Trends using a modeling approach that uses network-based text data (tweets). First, the popular trends are collected and stored in separate documents. These data are then pre-processed, followed by their labeling in respective categories. Data are then modeled and user interest for each Trending topic is calculated by considering positive tweets in that trend, average retweet and favorite count. Findings The proposed approach can be used to infer users’ topics of interest on Twitter and to categorize them. Support vector machine can be used for training and validation purposes. Positive tweets can be further analyzed to find user posting patterns. There is a positive correlation between tweets and Google data. Practical implications The results can be used in the development of information filtering and prediction systems, especially in personalized recommendation systems. Social implications Twitter microblogging platform offers content posting and sharing to billions of internet users worldwide. Therefore, this work has significant socioeconomic impacts. Originality/value This study guides on how Twitter network structure features can be exploited in discovering user interests using tweets. Further, positive correlation of Twitter Trends with Google Trends is reported, which validates the correctness of the authors’ approach.

Social media has become a platform of first choice where one can express his/her feelings with freedom. The sports and matches being played are also discussed on social media such as Twitter. In this article, efforts are made to investigate the feasibility of using collective knowledge obtained from microposts posted on Twitter to predict the winner of a Cricket match. For predictions, we use three different methods that depend on the total number of tweets before the game for each team, fans sentiments toward each team and fans score predictions on Twitter. By combining these three methods, we classify winning team prediction in a Cricket game before the start of game. Our results are promising enough to be used for winning team forecast. Furthermore, the effectiveness of supervised learning algorithms is evaluated where Support Vector Machine (SVM) has shown advantage over other classifiers.

Discovering frequent itemsets is a data analysis task used in numerous domains. It consists of finding sets of items (itemsets) that frequently appear in a set of database records (also called transactions). Though discovering frequent itemsets is useful, it can produce a large amount of spurious patterns. As a result, the user may spend a great amount of time to analyze the itemsets found by a frequent itemset mining algorithm to find truly interesting patterns. Hence, in recent years, a key research topic has emerged which is to discover statistically significant patterns in databases. The most popular model for identifying itemsets that are statistically significant is to discover non-redundant productive itemsets. The state-of-the-art algorithm to extract this set of patterns is OPUS-Miner. A key drawback of that algorithm is that it is designed to be applied to a static database. Moreover, a second drawback of OPUS-Miner is that it discovers all patterns in a database. In other words, the user cannot search for itemsets containing some specific items. This paper addresses these issues by defining the novel problem of discovering targeted non redundant productive itemsets in dynamic databases. An algorithm named IDPI+ (Interactive Discovery of Productive Itemsets) is presented, storing transactions in a tree structure, which can then be interactively queried to identify productive and non redundant itemsets containing specific items. A structure named Query-Tree is also introduced to process many queries at the same time. Moreover, to handle dynamic databases, efficient transaction insertion and deletion algorithms are provided to update the tree. It was observed in an experimental evaluation on benchmark datasets containing various types of data that IDPI+ can handle thousands of queries per second on a desktop computer. Moreover, it was found that IPDI+ is more than an order of magnitude faster than a baseline algorithm.

The proof development process in interactive theorem provers (ITPs) requires the users to manually search for proofs by interacting with proof assistants. The activity of finding the correct proofs can become quite cumbersome and time consuming for users. To make the proof searching process easier in proof assistants, we provide an evolutionary/heuristic-based framework. The basic idea for the framework is to first generate random proof sequences from a population of frequently occurring proof steps that are discovered with sequential pattern mining. Generated proof sequences are then evolved till their fitness match the fitness of the target (or original) proof sequences. Three algorithms based on the proposed framework are developed using the Genetic Algorithm (GA), Simulated Annealing (SA) and Particle Swarm Optimization (PSO). Extensive experiments are performed to investigate the performance of the proposed algorithms using the HOL4 proof assistant. Results have shown that the proposed algorithms can efficiently evolve the random sequences to obtain the target sequences. In comparison, PSO performed better than SA and SA performed better than GA. In general, the experimental results suggest that combining evolutionary/heuristic algorithms with proof assistants allow efficient support for proof finding/optimization.

Search engines and social networks are two entirely different data sources that can provide valuable information about Influenza. While search engine hosts can deliver popular queries (or terms) used for searching the Influenza related information, the social networks contain useful links of information sources that people have found valuable. The authors hypothesize that such data sources can provide vital first-hand information. In this article, they have proposed a methodology for detecting the information sources from social networks, particularly Twitter. The data filtering and source finding tasks are posed as classification tasks. Search engine queries are used for extracting related dataset. Results have shown that propose approach can be beneficial for extracting useful information regarding side effects, medications and to track geographical location of epidemics affected area.

Reo is a channel-based coordination language that allows the construction of connectors to coordinate behavior among different components in distributed systems. Probabilistic connectors in Reo capture the random and probabilistic behavior to deal with the uncertainty of the real world. In this paper we use PVS to provide a mechanical formalization for probabilistic connectors. We first present the formalization of random/probabilistic channels and the composition operators in PVS. Random and probabilistic channels are modeled as relations on timed data distribution sequences that are observed at the source and sink ends of these channels. Composition operators are used to combine random/probabilistic channels together with primitive channels to construct complex component connectors. The approach can be used to naturally specify complex connectors and prove important properties for probabilistic connectors as well as the refinement/equivalence relations between them with the PVS proof assistant.

Genetic Algorithms (GA) are bio-inspired algorithms that are now used in safety critical systems, robotics, artificial intelligence and bioinformatics, etc. A formal semantic model for GA is needed that can provide a framework for the modeling, reasoning and verification of GA based systems. On the other hand, Unifying Theories of Programming (UTP) offers formal semantic foundations for programming as well as specification languages. UTP is used in this paper to formalize a family of crossover and mutation operators of GA, where operators are defined as design models. UTP design models also allow the establishment of refinement and equivalence relations between GA operators by introducing implication between predicates. As an example, the equivalence relation between operators is proved with the PVS proof assistant.

Cloud computing enables one to access applications through Internet, without explicitly installing them on one single computing device. Formal modeling and verification of cloud services and their composition is fundamental to guarantee the accurate working and availability of cloud applications. In this paper, we use the Prototype Verification System (PVS) for formal modeling and verification of cloud services. Cloud services are modeled in PVS with the combination of logical predicates that represent the relations among the timed data sequences being observed at its input and output ports. Furthermore, composition operators are modeled that can be used to combine different cloud services together to construct more complex services. With our approach, properties of cloud services and refinement relations between different cloud services can be formalized as goals and proved with the PVS proof assistant.

Search engines and social media are two different online data sources where search engines can provide health related queries logs and Internet users' discuss their diseases, symptoms, causes, preventions and even suggest treatment by sharing their views, experiences and opinions on social media. This chapter hypothesizes that online data from Google and Twitter can provide vital first-hand healthcare information. An approach is provided for collecting twitter data by exploring contextual information gleaned from Google search queries logs. Furthermore, it is investigated that whether it is possible to use tweets to track, monitor and predict diseases, especially Influenza epidemics. Obtained results show that healthcare institutes and professional's uses social media to provide up-to date health related information and interact with public. Moreover, proposed approach is beneficial for extracting useful information regarding disease symptoms, side effects, medications and to track geographical location of epidemics affected area.

Formal modeling and verification of connectors in component-based software systems are getting more interest with recent advancements and evolution in modern software systems. In this paper, we use the proof assistant Coq for modeling and verification of timed connectors. We first present the definition of timed channels and the composition operators for constructing timed connectors in Coq. Basic timed channels are interpreted as axioms and inference rules are used for the specification of composition operators. Furthermore, timed connectors being built by composing basic timed/untimed channels, are defined as logical predicates which describe the relations between inputs and outputs. Within this framework, timed connector properties can be naturally formalized and proved in Coq.

New performance leaps has been achieved with multiprogramming and multi-core systems. Present parallel programming techniques and environment needs significant changes in programs to accomplish parallelism and also constitute complex, confusing and error-prone constructs and rules. Intel Cilk Plus is a C based computing system that presents a straight forward and well-structured model for the development, verification and analysis of multicore and parallel programming. In this article, two programs are developed using Intel Cilk Plus. Two sequential sorting programs in C/C++ language are converted to multi-core programs in Intel Cilk Plus framework to achieve parallelism and better performance. Converted program in Cilk Plus is then checked for various conditions using tools of Cilk and after that, comparison of performance and speedup achieved over the single-core sequential program is discussed and reported.

Analysis and finding errors in concurrent software/system particularly when it is used in safety or industrial critical systems is gaining more and more attention. Software testing is an important technique for finding errors, however for concurrent algorithms, testing often does not ensure correctness or absence of errors. The model checker SPIN is widely and successfully used to formally verify the correctness requirements for systems of concurrently executing processes. Software/system model is first developed in PROMELA modeling language and SPIN model checker accepts correctness claims that are declared as linear temporal logic (LTL) formulas. In this article, two famous concurrent algorithms for mutual exclusion problem (Bakery algorithm and Dekker algorithm) are analyzed and formally verified in SPIN. Mutual exclusion for both algorithms is verified with in-line assertion and as correctness claims with the help of LTL formulas. Furthermore, safety and liveness properties of both algorithms are verified with LTL formulas.