Coinduction is a proof rule which is the dual of induction. It allows reasoning about non-well-founded sets and is of particular use for reasoning about equivalences. In this thesis I present an automation of coinductive theorem proving. This automation is based on the ideas of proof planning [Bundy 88]. Proof planning as the name suggests, plans the higher level steps in a proof without performing the formal checking which is also required for a verification. The automation has focused on the use of coinduction to prove the equivalence of programs in a small lazy functional language which is similar to Haskell. One of the hardest parts in a coinductive proof is the choice of a relation, called a bisimulation. The automation here described makes an initial simplified guess at a bisimulation and then uses critics, revisions based on failure, and generalisation techniques to refine this guess. The proof plan for coinduction and the critic have been implemented in CLAM [Bundy et al 90b] with encouraging results. The planner has been successfully tested on a number of theorems. Comparison of the proof planner for coinduction with the proof plan for induction implemented in CLAM has gighlighted a number of equivalences and dualities in the process of these proofs and has also suggested improvements to both systems. This work has demonstrated not only the possibility of fully automated theorem provers for coinduction but has also demonstrated the uses of proof planning for comparison of proof techniques. This work has demonstrated not only the possibility of fully automated theorem provers for coinduction but has also demonstrated the uses of proof planning for comparison of proof techniques.

No description available.

No description available.

This research identifies and investigates major issues in inducing accurate and comprehensible fuzzy rules from datasets. A review of the current literature on fuzzy rulebase induction uncovers two significant issues: A. There is a tradeoff between inducing accurate fuzzy rules and inducing comprehensible fuzzy rules; and, B. A common strategy for the induction of fuzzy rulebases, that of iterative rule learning where the rules are generated one by one and independently of each other, may not be an optimal one. FRANTIC, a system that provides a framework for exploring the claims above is developed. At the core lies a mechanism for creating individual fuzzy rules. This is based on a significantly modified social insect-inspired heuristic for combinatorial optimisation -- Ant Colony Optimisation. The rule discovery mechanism is utilised in two very different strategies for the induction of a complete fuzzy rulebase: 1. The first follows the common iterative rule learning approach for the induction of crisp and fuzzy rules; 2. The second has been designed during this research explicitly for the induction of a fuzzy rulebase, and generates all rules in parallel. Both strategies have been tested on a number of classification problems, including medical diagnosis and industrial plant fault detection, and compared against other crisp or fuzzy induction algorithms that use more well-established approaches. The results challenge statement A above, by presenting evidence to show that one criterion need not be met at the expense of the other. This research also uncovers the cost that is paid -- that of computational expenditure -- and makes concrete suggestions on how this may be resolved. With regards to statement B, until now little or no evidence has been put forward to support or disprove the claim. The results of this research indicate that definite advantages are offered by the second simultaneous strategy, that are not offered by the iterative one. These benefits include improved accuracy over a wide range of values for several key system parameters. However, both approaches also fare well when compared to other learning algorithms. This latter fact is due to the rule discovery mechanism itself -- the adapted Ant Colony Optimisation algorithm -- which affords several additional advantages. These include a simple mechanism within the rule construction process that enables it to cope with datasets that have an imbalanced distribution between the classes, and another for controlling the amount of fit to the training data. In addition, several system parameters have been designed to be semi-autonomous so as to avoid unnecessary user intervention, and in future work the social insect metaphor may be exploited and extended further to enable it to deal with industrial-strength data mining issues involving large volumes of data, and distributed and/or heterogeneous databases.

An Extension to the Composite Rule Induction System Discovering knowledge from data is an important task for knowledge management and development of intelligent systems, which is called knowledge acquisition or data mining. Many techniques have been developed for such purpose. For example, ID3, C4.5 (tree induction techniques) and Artificial Neural Networks are among the popular techniques in ¡§Classification and Prediction¡¨ area. However, these methods often use the same criteria to analyze nominal and non-nominal attributes, which is very likely to produce biased knowledge due to mis-match between data type and their algorithms. In Liang (1992), he proposed a composite approach called CRIS to inducing knowledge that introduces statistical concepts and data mining heuristics and found the composite method outperformed other methods including tree induction, discriminant analysis, and neural networks. However, the paper focuses on the classification of binary objects and did not describe how the approach can be applied to a problem with more than two classes in the dependent variable. In this research, we extend the previous approach to solve the problem with more than two classes. We also enhance the approach by adding steps to prioritizing attributes using their identification power and controlling the growth of generated hypothesis. In order evaluate the extended CRIS method, a prototype system, eCRIS, was developed and compared with a commercial data mining package, XLMiner3 (developed by Cytel Software Corporation) using three existing datasets in data mining research. The results indicate that the extended CRIS outperforms tree induction and backpropagation in neural networks in datasets that include both nominal and non-nominal data and performed equally well with them.

With the computerization of businesses, more and more data are generated and stored in databases for many business applications. Finding interesting patterns among those data may lead to useful knowledge that provides competitive advantage in business. Knowledge discovery in database has thus become an important issue to help business acquire knowledge that assists managerial and operational work. Among many types of knowledge, classification knowledge is widely used. Most classification rules learned by induction algorithms are in the crisp form. Fuzzy linguistic representation of rules, however, is much closer to the way human reasons. The objective of this research is to propose a method to mine classification knowledge from the database with fuzzy descriptions. The procedure contains five steps, starting from data preparation to rule pruning. A rule induction algorithm, RITIO, is employed to generate the classification rules. Fuzzy inference mechanism that includes fuzzy matching and output reasoning is specified to yield the output class. An experiment is conducted using several databases to show advantages of this work. The proposed method is justified with good system performance. It can be easily implemented in various business applications on classification tasks.

Rule induction is a popular technique for knowledge acquisition and data mining. Many techniques, such as ID3, C4.5, CART (tree induction tecniques) and Artificial Neural Networks have been developed and widely used. However, most techniques are either based on categorical or numerical mechanisms to assess the importance of different input variables, which may not produce the optimal rule when a mixture of variables exists. In 1992, Liang proposed a composite approach called CRIS that use different method to analyze different types of data in inducing rules for binary classification. Yang conducted a follow-up research to extend the original algorithm to multiple categories. However, both methods do not take variable interaction into consideration. The purpose of this research is to extend previous approach and extend by including second-order interaction. We also take into consideration the kurtosis and skewness of data for numerical variables. For categorical data, we also adopt ID3 algorithm to handle classes with low representation in the sample. In order to evaluate this technique, we develop a prototype CRIS 3.0 and compare with existing techniques, including multi-category-CRIS, CART and C4.5 as benchmark. The results show that CRIS 3.0 has the highest probability of producing the highest prediction accuracy.

The Composite Rule Induction System proposed by Liang (1992) that uses the tabular approach and statistical inference to process qualitative and quantitative attributes separately for generating better classification rules. Yang (2007) extended the method by incorporating the second-order rules. This Study further extends the previous method by including a mechanism for detecting the existence of interaction effects. The detection method checks the degree of independence between attributes to determine whether the second-order rules should be processed. In order to evaluate the performance of the proposed method, an enhanced prototype system was developed and both real and simulated data were used to compare its accuracy and rule complexity with existing systems. The result shows that the enhanced system performs at least as accurate as the existing system but is significantly better in the complexity of the resulting knowledge base.

In the last several years the number of computer network attacks has increased rapidly, while at the same time the attacks have become more and more complex and sophisticated. Intrusion detection systems (IDSs) have become essential security appliances for detecting and reporting these complex and sophisticated attacks. Security officers and analysts need to analyze intrusion alerts in order to extract the underlying attack scenarios and attack intelligence. These allow taking appropriate responses and designing adequate defensive or prevention strategies. Intrusion analysis is a resource intensive, complex and expensive process for any organization. The current generation of IDSs generate low level intrusion alerts that describe individual attack events. In addition, existing IDSs tend to generate massive amount of alerts with high rate of redundancies and false positives. Typical IDS sensors report attacks independently and are not designed to recognize attack plans or discover multistage attack scenarios. Moreover, not all the attacks executed against the target network will be detected by the IDS. False negatives, which correspond to the attacks missed by the IDS, will either make the reconstruction of the attack scenario impossible or lead to an incomplete attack scenario. Because of the above mentioned reasons, intrusion analysis is a challenging task that mainly relies on the analyst experience and requires manual investigation. In this dissertation, we address the above mentioned challenges by proposing a new framework that allows automatic intrusion analysis and attack intelligence extraction by analyzing the alerts and attacks semantics using both machine learning and knowledge-representation approaches. Particularly, we use ontological engineering, semantic correlation, and clustering methods to design a new automated intrusion analysis framework. The proposed alert analysis approach addresses many of the gaps observed in the existing intrusion analysis techniques, and introduces when needed new metrics to measure the quality of the alerts analysis process. We evaluated experimentally our framework using different benchmark intrusion detection datasets, yielding excellent performance results. / Graduate

Matrix inductive reasoning has been a popular research topic due to its claimed relationship with the general factor of intelligence. In this research, four subabilities were identified: working memory, rule induction, rule application, and figure detection. This quantitative study examined the relationship between these four subabilites and students' general ability to solve Matrix Reasoning problems. Using tests developed for this research to measure the identified subabilities, the data were collected from 334 Chinese students aged from 12 to 15. Structural equation modeling method was used to analyze the collected data and to evaluate the hypothesized models. Results from the analysis showed that a valid model existed to represent the construct of matrix inductive reasoning. Except for figural detection ability, the other three subabilities had significant direct effects on matrix inductive reasoning ability. Readers should interpret from this result with caution due to the unsatisfactory reliability of the Figure Detection scores. To improve the validity of the interpretation, a new model without the latent variable of figure detection was reexamined. In this analysis, significant relationships still existed from the three subablities to matrix inductive reasoning ability. The strongest relationship existed from working memory ability to matrix reasoning ability, with a standardized coefficient of .52. Effects from rule induction and rule application ability to matrix reasoning dropped to .36 and .34 respectively. These results suggested the important role of working memory on solving inductive reasoning problems. In addition, a significant and substantial indirect path was found that lead from working memory to rule induction to rule application to matrix reasoning. The indirect path indicated that a process existed when students solved Matrix Reasoning tasks.