No description available.

No description available.

It is possible to implement mathematical proofs in a machine-readable language. Indeed, certain proofs, especially those deriving properties of safety-critical systems, are often required to be checked by machine in order to avoid human errors. However, machine checkable proofs are very hard to follow by a human reader. Because of their unreadability, such proofs are hard to implement, and more difficult still to maintain and modify. In this thesis we study the possibility of implementing machine checkable proofs in a more readable format. We design a declarative proof language, SPL, which is based on the Mizar language. We also implement a proof checker for SPL which derives theorems in the HOL system from SPL proof scripts. The language and its proof checker are extensible, in the sense that the user can modify and extend the syntax of the language and the deductive power of the proof checker during the mechanisation of a theory. A deductive database of trivial knowledge is used by the proof checker to derive facts which are considered trivial by the developer of mechanised theories so that the proofs of such facts can be omitted. We also introduce the notion of structured straightforward justifications, in which simple facts, or conclusions, are justified by a number of premises together with a number of inferences which are used in deriving the conclusion from the given premises. A tableau prover for first-order logic with equality is implemented as a HOL derived rule and used during the proof checking of SPL scripts. The work presented in this thesis also includes a case study involving the mechanisation of a number of results in group theory in SPL, in which the deductive power of the SPL proof checker is extended throughout the development of the theory.

Visualization or Visualization in Scientific Computing is a rapidly growing area in computer science. Visualization is the process and result of viewing data and numbers as a diagram or drawing. Arie Kaufman sums up visualization by stating: ``It encompasses and unifies the fields of Computer Graphics, image processing, computer vision, signal processing, computer aided design, and human-machine interaction. Visualization is a method of extracting meaningful information from complex or voluminous datasets through the use of interactive graphics and imaging. It provides processes for steering the dataset and seeing the unseen, thereby enriching existing scientific methods'', (Arie Kaufman, Preface, Visualization '90). Over the past few years visualization has spread into multiple disciplines and many diverse visualization systems and environments have been designed. This thesis describes many aspects of visualization, focusing on Abstractional visualization. An abstraction in terms of computer graphics and visualization is an image that has been transformed from an original form; often the abstraction is created by losing one or more features from the original instance. For example, the London Underground map is an abstraction of the geographical map (itself in turn an abstraction of the `real' landmarks). The design of the underground map loses the exact positioning information of each of the stations; the connectivity of the railway tracks remains however and the map can be said to be clearer and easier to understand than the original geographical map -- it has been simplified. This thesis describes aspects of visualization using this abstraction idea.

Multimedia services envisaged for high speed networks may have large numbers of users, require high volumes of network resources and have real-time delay constraints. For these reasons, several multicast routing heuristics that use two link metrics have been proposed with the objective of minimising multicast tree cost while maintaining a bound on delay. Previous evaluation work has compared the relative average performance of some of these heuristics and concludes that they are generally efficient. This thesis presents a detailed analysis and evaluation of these heuristics which illustrate that in some situations their average performance is prone to wide variance for a particular multicast in a specific network. It concludes that the efficiency of an heuristic solution depends on the topology of both the network and the multicast, which is difficult to predict. The integration of two heuristics with Dijkstras shortest path tree algorithm is proposed, to produce a hybrid that consistently generates efficient multicast solutions for all possible multicast groups in any network. The evaluation results show good performance over a wide range of networks (flat and hierarchical) and multicast groups, within differing delay bounds. The more efficient the multicast tree is, the less stable it will be as multicast group membership changes. An efficient heuristic is extended to ensure multicast tree stability where multicast group membership is dynamic. This extension decreases the efficiency of the heuristics solutions, although they remain significantly cheaper than the worst case, a shortest delay path tree. This thesis also discusses how the hybrid and the extended heuristic might be applied to multicast routing protocols for the Internet and ATM Networks. Additionally, the behaviour of the heuristics is examined in networks that use a single link metric to calculate multicast trees and concludes one of the heuristics may be of benefit in such networks.

This thesis deals with two themes: (1) construction of abstract domains for mode analysis of typed logic programs; (2) verification of logic programs using non-standard selection rules. (1) Mode information is important mainly for compiler optimisations. The precision of a mode analysis depends partly on the expressiveness of the abstract domain. We show how specialised abstract domains may be constructed for each type in a typed logic program. These domains capture the degree of instantiation of a term very precisely. The domain construction procedure is implemented using the Godel language and tested on some example programs to demonstrate the viability and high precision of the analysis. (2) We provide verification methods for logic programs using selection rules other than the usual left-to-right selection rule. We consider five aspects of verification: termination; and freedom from (full) unification, occur-check, foundering, and errors related to built-ins. The methods are based on assigning a mode, input or output, to each argument position of each predicate. This mode is only fixed with respect to a particular execution. For termination, we first identify a class of predicates which terminate under the assumption that derivations are input-consuming, meaning that in each derivation step, the input arguments of the selected atom do not become instantiated. Input-consuming derivations can be realised using block declarations, which test that certain argument positions of the selected atom are non-variable. To show termination for a program where not all predicates terminate under the assumption that derivations are input-consuming, we make the stronger assumption that derivations are left-based. This formalises the ''default left-to-right'' selection rule of Prolog. To the best of our knowledge, this work is the first formal and comprehensive approach to this kind of termination problem. The results on the other four aspects are mainly generalisations of previous results assuming the left-to-right selection rule.

With the continuing drop in the price of memory, Video-on-Demand (VoD) solutions that have so far focused on maximising the throughput of disk units with a minimal use of physical memory may now employ significant amounts of cache memory. The subject of this thesis is the study of a technique to best utilise a memory buffer within such a VoD solution. In particular, knowledge of the streams active on the server is used to allocate cache memory. Stream optimised caching exploits reuse of data among streams that are temporally close to each other within the same clip; the data fetched on behalf of the leading stream may be cached and reused by the following streams. Therefore, only the leading stream requires access to the physical disk and the potential level of service provision allowed by the server may be increased. The use of stream optimised caching may consequently be limited to environments where reuse of data is significant. As such, the technique examined within this thesis focuses on a classroom environment where user progress is generally linear and all users progress at approximately the same rate for such an environment, reuse of data is guaranteed. The analysis of stream optimised caching begins with a detailed theoretical discussion of the technique and suggests possible implementations. Later chapters describe both the design and construction of a prototype server that employs the caching technique, and experiments that use of the prototype to assess the effectiveness of the technique for the chosen environment using `emulated' users. The conclusions of these experiments indicate that stream optimised caching may be applicable to larger scale VoD systems than small scale teaching environments. Future development of stream optimised caching is considered.

No description available.

No description available.

No description available.