No description available.

No description available.

No description available.

This thesis is concerned with algorithms for generating generalisations-from experience. These algorithms are viewed as examples of the general concept of a hypothesis discovery system which, in its turn, is placed in a framework in which it is seen as one component in a multi-stage process which includes stages of hypothesis criticism or justification, data gathering and analysis and prediction. Formal and informal criteria, which should be satisfied by the discovered hypotheses are given. In particular, they should explain experience and be simple. The formal work uses the first-order predicate calculus. These criteria are applied to the case of hypotheses which are generalisations from experience. A formal definition of generalisation from experience, relative to a body of knowledge is developed and several syntactical simplicity measures are defined. This work uses many concepts taken from resolution theory (Robinson, 1965). We develop a set of formal criteria that must be satisfied by any hypothesis generated by an algorithm for producing generalisation from experience. The mathematics of generalisation is developed. In particular, in the case when there is no body of knowledge, it is shown that there is always a least general generalisation of any two clauses, in the generalisation ordering. (In resolution theory, a clause is an abbreviation for a disjunction of literals.) This least general generalisation is effectively obtainable. Some lattices induced by the generalisation ordering, in the case where there is no body of knowledge, are investigated. The formal set of criteria is investigated. It is shown that for a certain simplicity measure, and under the assumption that there is no body of knowledge, there always exist hypotheses which satisfy them. Generally, however, there is no algorithm which, given the sentences describing experience, will produce as output a hypothesis satisfying the formal criteria. These results persist for a wide range of other simplicity measures. However several useful cases for which algorithms are available are described, as are some general properties of the set of hypotheses which satisfy the criteria. Some connections with philosophy are discussed. It is shown that, with sufficiently large experience, in some cases, any hypothesis which satisfies the formal criteria is acceptable in the sense of Hintikka and Hilpinen (1966). The role of simplicity is further discussed. Some practical difficulties which arise because of Goodman's (1965) "grue" paradox of confirmation theory are presented. A variant of the formal criteria suggested by the work of Meltzer (1970) is discussed. This allows an effective method to be developed when this was not possible before. However, the possibility is countenanced that inconsistent hypotheses might be proposed by the discovery algorithm. The positive results on the existence of hypotheses satisfying the formal criteria are extended to include some simple types of knowledge. It is shown that they cannot be extended much further without changing the underlying simplicity ordering. A program which implements one of the decidable cases is described. It is used to find definitions in the game of noughts and crosses and in family relationships. An abstract study is made of the progression of hypothesis discovery methods through time. Some possible and some impossible behaviours of such methods are demonstrated. This work is an extension of that of Gold (1967) and Feldman (1970). The results are applied to the case of machines that discover generalisations. They are found to be markedly sensitive to the underlying simplicity ordering employed.

In an attempt to overcome the great inefficiency of theorem proving methods, several existing methods are studied, and several now ones are proposed. A concentrated attempt is made to devise a unified proof procedure whose inference rules are designed for the efficient use by a search strategy. For unsatisfiable sets of Horn clauses, it is shown that p1-resolution and selective linear negative (SLN) resolution can be alternated heuristically to conduct a bi-directional search. This bi-directional search is shown to be more efficient than either of P.-resolution and SLN-resolution. The extreme sparseness of the SLN-search spaces lead to the extension of SLN-resolution to a more general and more powerful resolution rule, selective linear (SL) resolution, which resembles Loveland's model elimination strategy. With SL-resolution, all immediate descendants of a clause are obtained by resolving upon a single selected literal of that clause. Linear resolution, s-linear resolution and t-linear resolution are shown to be as powerful as the most powerful resolution systems. By slightly decreasing the power, considerable increase in the sparseness of search spaces is obtained by using SL-resolution. The amenability of SL-resolution to applications of heuristic methods suggest that, on these grounds alone, it is at least competitive with theorem-proving procedures designed solely from heuristic considerations. Considerable attention is devoted to various anticipation procedures which allow an estimate of the sparseness of search trees before their generation. Unlimited anticipation takes the form of pseudo-search trees which construct outlines of possible proofs. Anticipation procedures together with a number of heuristic measures are suggested for the implementation of an exhaustive search strategy for SL-resolution.

This thesis was motivated by a case study involving the formalisation of arguments that simplify the verification of tree-oriented multicast protocols. As well as covering the case study itself, it discusses our solution to problems we encountered concerning expressivity and automation. The expressivity problems related to the need for theory interpretation. We found the existing Locale and axiomatic type class mechanisms provided by the Isabelle theorem prover we were using to be inadequate. This led us to develop a new prototype implementation of theory interpretation. To support this implementation, we developed a novel system of proof terms for the HOL logic that we also describe in this thesis. We found existing automation to perform poorly, which led us to experiment with additional kinds of automation. We describe our approach, focusing on features that make automation suitable for interactive use. Our presentation of the case study starts with our formalisation of an abstract theory of distributed systems, covering state transition systems, forward and backward simulation relations, and related properties of LTL (linear temporal logic). We then summarise proofs of simulation relations holding for particular abstract multicast protocols. We discuss the mechanisation styles we experimented with in the case study. We also discuss the methodology behind our proofs. We cover aspects such as how to discover and construct proofs, and how to explore the space of proofs, how to make good definitions and lemmas, how to increase modularity, reuse, stability and malleability of proofs, and reduce maintenance of proofs, and the gap between intuitively understood proofs and their formalisation.

In 1943, Littlewood and Offord proved the first anti-concentration result for sums of independent random variables. Their result has since then been strengthened and generalised by generations of researchers, with applications in several areas of mathematics. In this paper, we present the first non-abelian analogue of the Littlewood Offord result, a sharp anti-concentration inequality for products of independent random variables. (C) 2016 Elsevier Inc. All rights reserved.

The purpose of this paper is to derive certain of the fundamental properties of the Dini derivatives of an arbitrary real function. To this end it will be necessary to investigate the properties of the limits superior and inferior of real functions and to prove the Vitali Covering Theorem as well as a fundamental theorem on the metric density of arbitrary point sets.

In this thesis we study the thin-film type equations in one spatial dimension. These equations arise from the lubrication approximation to the thin films of viscous fluids which is described by the Navier-Stokes equations with free boundary. From the structural point of view, they are fourth-order degenerate nonlinear parabolic equations, with principal term from diffusion and lower order term from external forces. In Chapter one we study the dynamics of the equations when the external force is given by a power law. Classification of steady states of this equation, which is important for the dynamics, was already known. Previous numerical studies show that there is a mountain pass scenario among the steady states. We shall provide a rigorous justification to these numerical results. As a result, a rather complete picture of the dynamics of the thin film is obtained when the power law is in the range (1,3). In Chapter two we turn to the special case of the equation where the external force is the gravity. This is important, but, unfortunately not a power law. We study and classify the steady states of this equation as well as compare their energy levels. Some numerical results are also present. / Zhang, Zhenyu. / Asviser: Kai Seng Chou. / Source: Dissertation Abstracts International, Volume: 73-06, Section: B, page: . / Thesis (Ph.D.)--Chinese University of Hong Kong, 2011. / Includes bibliographical references (leaves 103-107). / Electronic reproduction. Hong Kong : Chinese University of Hong Kong, [2012] System requirements: Adobe Acrobat Reader. Available via World Wide Web. / Electronic reproduction. [Ann Arbor, MI] : ProQuest Information and Learning, [201-] System requirements: Adobe Acrobat Reader. Available via World Wide Web. / Abstract also in Chinese.

Tang Ko Cheung, Simon. / Thesis (M.Phil.)--Chinese University of Hong Kong, 2001. / Includes bibliographical references (leaves 89-91). / Abstracts in English and Chinese. / Chapter 1 --- Theory of Optimal Normal Bases --- p.3 / Chapter 1.1 --- Introduction --- p.3 / Chapter 1.2 --- The minimum number of terms --- p.6 / Chapter 1.3 --- Constructions for optimal normal bases --- p.7 / Chapter 1.4 --- Existence of optimal normal bases --- p.10 / Chapter 2 --- Implementing Multiplication in GF(2m) --- p.13 / Chapter 2.1 --- Defining the Galois fields GF(2m) --- p.13 / Chapter 2.2 --- Adding and squaring normal basis numbers in GF(2m) --- p.14 / Chapter 2.3 --- Multiplication formula --- p.15 / Chapter 2.4 --- Construction of Lambda table for Type I ONB in GF(2m) --- p.16 / Chapter 2.5 --- Constructing Lambda table for Type II ONB in GF(2m) --- p.21 / Chapter 2.5.1 --- Equations of the Lambda matrix --- p.21 / Chapter 2.5.2 --- An example of Type IIa ONB --- p.23 / Chapter 2.5.3 --- An example of Type IIb ONB --- p.24 / Chapter 2.5.4 --- Creating the Lambda vectors for Type II ONB --- p.26 / Chapter 2.6 --- Multiplication in practice --- p.28 / Chapter 3 --- Inversion over optimal normal basis --- p.33 / Chapter 3.1 --- A straightforward method --- p.33 / Chapter 3.2 --- High-speed inversion for optimal normal basis --- p.34 / Chapter 3.2.1 --- Using the almost inverse algorithm --- p.34 / Chapter 3.2.2 --- "Faster inversion, preliminary subroutines" --- p.37 / Chapter 3.2.3 --- "Faster inversion, the code" --- p.41 / Chapter 4 --- Elliptic Curve Cryptography over GF(2m) --- p.49 / Chapter 4.1 --- Mathematics of elliptic curves --- p.49 / Chapter 4.2 --- Elliptic Curve Cryptography --- p.52 / Chapter 4.3 --- Elliptic curve discrete log problem --- p.56 / Chapter 4.4 --- Finding good and secure curves --- p.58 / Chapter 4.4.1 --- Avoiding weak curves --- p.58 / Chapter 4.4.2 --- Finding curves of appropriate order --- p.59 / Chapter 5 --- The performance of 17x bit Elliptic Curve Scalar Multiplication --- p.63 / Chapter 5.1 --- Choosing finite fields --- p.63 / Chapter 5.2 --- 17x bit test vectors for onb --- p.65 / Chapter 5.3 --- Testing methodology and sample runs --- p.68 / Chapter 5.4 --- Proposing an elliptic curve discrete log problem for an 178bit curve --- p.72 / Chapter 5.5 --- Results and further explorations --- p.74 / Chapter 6 --- On matrix RSA --- p.77 / Chapter 6.1 --- Introduction --- p.77 / Chapter 6.2 --- 2 by 2 matrix RSA scheme 1 --- p.80 / Chapter 6.3 --- Theorems on matrix powers --- p.80 / Chapter 6.4 --- 2 by 2 matrix RSA scheme 2 --- p.83 / Chapter 6.5 --- 2 by 2 matrix RSA scheme 3 --- p.84 / Chapter 6.6 --- An example and conclusion --- p.85 / Bibliography --- p.91