A Computer-Assisted sentence Stress Teaching and Learning Environment (CASTLE) is proposed and developed, in order to help learners of English as a Second Language (ESL) to perceive and produce English stress correctly. Sentence stress plays an important role in English verbal communication. Incorrect stress may confuse listeners, and even break down a conversation. Stress is also challenging for ESL learners to master. It is neither easy for them to produce nor easy to perceive stress. Learners tend to transfer the stress patterns of their first language into English, which is not always appropriate. However, stress has been overlooked in English language teaching classes, due to the time limits of a class and teachers’ lack of confidence of teaching stress. Thus, CASTLE is intended to help ESL learners to use sentence stress correctly. There are three modules in CASTLE: an individualised speech learning material providing module, a perception assistance module and a production assistance module. Through conducting an investigation into which voice features (i.e. gender, pitch and speech rate) makes a teacher’s voice preferable for learners to imitate, we find that learners’ imitation preferences vary, according to many factors (e.g. English background and language proficiency). Thus, the speech material providing module of CASTLE can provide individualised speech material for different learners, based on their preferred voice features. In the perception assistance module of CASTLE, we propose a set of stress exaggeration methods that can automatically enlarge the differences between stressed and unstressed syllables in teachers’ voice. These stress exaggeration methods are implemented by the manipulation of different prosodic features (i.e. pitch, duration and intensity) of the teachers’ voice. Our experimental results show that all our proposed exaggeration methods could help ESL learners to perceive sentence stress more accurately. In the production assistance module of CASTLE, we propose a clapping-based sentence stress practice model that is intended to help ESL learners to be aware of the rhythm of English language. By analysing the limitation of conventional categorical representation of stress, we propose a fuzzy representation which is intended to better represent the subjective nature of stress. Based on the fuzzy representation of stress, we propose three feedback models in order to help the learners correct their stress errors. In addition to the development of CASTLE, we also propose an enhanced fuzzy linear regression model which can overcome the spreads increasing problem encountered by previous fuzzy linear regression models.

The focus of this research is to investigate the potential of user interface (UI) pattern languages in assisting students of Human Computer Interaction (HCI) to learn the principles of UI design. A graphical representation named a UI-pattern model was developed. It arose from the evaluation of four existing pattern languages. The UI-pattern model is an enhanced form of UI pattern list that represents a specific UI. It was recognised that the UI-pattern model has the potential to help students learn about pattern language structure. It was also realised that UI-pattern modelling can be used to incrementally improve pattern languages through the generative process proposed by Alexander (1979). A UI pattern language Maturity Model (UMM) has been developed. This model can be used by educators when selecting and/or modifying existing UI pattern languages so that they are more appropriate for student use. A method for developing detailed UI designs that utilises a UI pattern language has been developed with the aim of providing students with an ‘authentic’ real-world UI design experience, as envisaged by constructivist educational theory (Jonassen 1999). This UI design method (TUIPL) guides the students’ development of user interface conceptual models. To establish the authenticity of TUIPL three case studies were undertaken out with developers who had differing levels of UI design experience. A series of studies investigated how HCI students used TUIPL to guide the development of UI-pattern models and canonical abstract prototypes. The studies also ascertained the students’ views on using three different forms of UI pattern (illustrated, narrative and diagrammed). Data was collected by observation, questionnaires and completed exercises. The results indicate that the students developed an understanding of pattern language structure, were positive about their experience building UI-pattern models and canonical abstract prototypes, and that patterns aided communication. The learning outcomes were encouraging and students responded positively to using a UI pattern language.

To support extramural learning, Johnson (2005) has proposed the Learning Computer concept, which aims to provide a learning appliance that can be used for studying university courses at any time, from anywhere, and by anybody who might have only basic software and hardware, dial-up Internet connection, and little computer literacy. Lonely extramural students need extra support for interactions and collaboration in learning, especially in second language learning that requires intensive oral language practice between the students and the tutor. This research project was a trial to extend IMMEDIATE (the prototype of the Learning Computer) to a second language extramural course. To meet the requirements of long distance conversation in such a course, a synchronous/asynchronous bimodal approach was conceptualised based on a review of e-learning, communication, and VoIP technologies. It was proposed that the prototype should automatically adapt to either synchronous mode or asynchronous mode according to different levels of Internet connection speed. An asynchronous conversation mode similar to Push-to-Talk (PTT) was also proposed. A VoIP SDK was investigated and used in the prototype for fast development. IMMEDIATE messaging protocols have been extended in the prototype to control call procedures and the asynchronous conversation mode. An evaluation of the prototype which was conducted to assess its usability, functionality and integrity of the prototype demonstrated that users can conduct telephone-like synchronous conversation efficiently at high connection speed. Although the PTT-like asynchronous mode has a time lag problem, especially when two users are both at low connection speed, it is a still a good way for novices to practise second language oral skills. The evaluation has given strongly support to the feasibility and effectiveness of the bimodal approach for applying IMMEDIATE in second language extramural learning.

We investigate the expressive power of different fragments of higher-order logics over finite relational structures (or equivalently, relational databases) with special emphasis in higher-order logics of order greater than or equal three. Our main results concern the study of the effect on the expressive power of higher-order logics, of simultaneously bounding the arity of the higher-order variables and the alternation of quantifiers. Let AAi(r,m) be the class of (i + 1)-th order logic formulae where all quantifiers are grouped together at the beginning of the formulae, forming m alternating blocks of consecutive existential and universal quantifiers, and such that the maximal-arity (a generalization of the concept of arity, not just the maximal of the arities of the quantified variables) of the higher-order variables is bounded by r. Note that, the order of the quantifiers in the prefix may be mixed. We show that, for every i [greater than or equal to] 1, the resulting AAi hierarchy of formulae of (i + 1)-th order logic is proper. This extends a result by Makowsky and Pnueli who proved that the same hierarchy in second-order logic is proper. In both cases the strategy used to prove the results consists in considering the set AUTOSAT(F) of formulae in a given logic F which, represented as finite structures, satisfy themselves. We then use a similar strategy to prove that the classes of [Sigma superscript i subscript m union Pi superscript i subscript m] formulae in which the higher-order variables of all orders up to i+1 have maximal-arity at most r, also induce a proper hierarchy in each higher-order logic of order i [greater than or equal to] 3. It is not known whether the correspondent hierarchy in second-order logic is proper. Using the concept of finite model truth definitions introduced by M. Mostowski, we give a sufficient condition for that to be the case. We also study the complexity of the set AUTOSAT(F) and show that when F is one of the prenex fragments [Sigma superscript 1 subscript m] of second-order logic, it follows that AUTOSAT(F) becomes a complete problem for the corresponding prenex fragment [Sigma superscript 2 subscript m] of third-order logic. Finally, aiming to provide the background for a future line of research in higher-order logics, we take a closer look to the restricted second-order logic SO[superscript w] introduced by Dawar. We further investigate its connection with the concept of relational complexity studied by Abiteboul, Vardi and Vianu. Dawar showed that the existential fragment of SO[superscript w] is equivalent to the nondeterministic inflationary fixed-point logic NFP. Since NFP captures relational NP, it follows that the existential fragment of SO[superscript w] captures relational NP. We give a direct proof, in the style of the proof of Fagin’s theorem, of this fact. We then define formally the concept of relational machine with relational oracle and prove the exact correspondence between the prenex fragments of SO[superscript w] and the levels of the relational polynomial-time hierarchy. This allows us to stablish a direct connection between the relational polynomial hierarchy and SO without using the Abiteboul and Vianu normal form for relational machines.

We investigate the expressive power of different fragments of higher-order logics over finite relational structures (or equivalently, relational databases) with special emphasis in higher-order logics of order greater than or equal three. Our main results concern the study of the effect on the expressive power of higher-order logics, of simultaneously bounding the arity of the higher-order variables and the alternation of quantifiers. Let AAi(r,m) be the class of (i + 1)-th order logic formulae where all quantifiers are grouped together at the beginning of the formulae, forming m alternating blocks of consecutive existential and universal quantifiers, and such that the maximal-arity (a generalization of the concept of arity, not just the maximal of the arities of the quantified variables) of the higher-order variables is bounded by r. Note that, the order of the quantifiers in the prefix may be mixed. We show that, for every i [greater than or equal to] 1, the resulting AAi hierarchy of formulae of (i + 1)-th order logic is proper. This extends a result by Makowsky and Pnueli who proved that the same hierarchy in second-order logic is proper. In both cases the strategy used to prove the results consists in considering the set AUTOSAT(F) of formulae in a given logic F which, represented as finite structures, satisfy themselves. We then use a similar strategy to prove that the classes of [Sigma superscript i subscript m union Pi superscript i subscript m] formulae in which the higher-order variables of all orders up to i+1 have maximal-arity at most r, also induce a proper hierarchy in each higher-order logic of order i [greater than or equal to] 3. It is not known whether the correspondent hierarchy in second-order logic is proper. Using the concept of finite model truth definitions introduced by M. Mostowski, we give a sufficient condition for that to be the case. We also study the complexity of the set AUTOSAT(F) and show that when F is one of the prenex fragments [Sigma superscript 1 subscript m] of second-order logic, it follows that AUTOSAT(F) becomes a complete problem for the corresponding prenex fragment [Sigma superscript 2 subscript m] of third-order logic. Finally, aiming to provide the background for a future line of research in higher-order logics, we take a closer look to the restricted second-order logic SO[superscript w] introduced by Dawar. We further investigate its connection with the concept of relational complexity studied by Abiteboul, Vardi and Vianu. Dawar showed that the existential fragment of SO[superscript w] is equivalent to the nondeterministic inflationary fixed-point logic NFP. Since NFP captures relational NP, it follows that the existential fragment of SO[superscript w] captures relational NP. We give a direct proof, in the style of the proof of Fagin’s theorem, of this fact. We then define formally the concept of relational machine with relational oracle and prove the exact correspondence between the prenex fragments of SO[superscript w] and the levels of the relational polynomial-time hierarchy. This allows us to stablish a direct connection between the relational polynomial hierarchy and SO without using the Abiteboul and Vianu normal form for relational machines.

This research work is focused on understanding the effects of inhomogeneity on traffic flow by theoretical analysis and computer simulations. Traffic has been observed at almost all levels of natural and manmade systems (e.g., from microscopic protein motors to macroscopic objects like cars). For these various traffic, basic and emer- gent phenomena, modelling methods, theoretical analysis and physical meanings are normally concerned. Inhomogeneity like bottlenecks may cause traffic congestions or motor protein crowding. The crowded protein motors may lead to some human diseases. The congested traffic patterns have not been understood well so far. The modelling method in this research is based on totally asymmetric simple exclusion process (TASEP). The following TASEP models are developed: TASEP with single inhomogeneity, TASEP with zoned inhomogeneity, TASEP with junction, TASEP with site sharing and different boundary conditions. These models are motivated by vehicular traffic, pedestrian trafficc, ant traffic, protein motor traffic and/or Internet traffic. Theoretical solutions for the proposed models are obtained and verified by Monte Carlo simulations. These theoretical results can be used as a base for further developments. The emergent properties such as phase transitions, phase separations and spontaneous symmetry breaking are observed and discussed. This study has contributed to a deeper understanding of generic traffic dynamics, particularly, in the presence of inhomogeneity, and has important implications for explanation or guidance of future traffic studies.

We investigate the expressive power of different fragments of higher-order logics over finite relational structures (or equivalently, relational databases) with special emphasis in higher-order logics of order greater than or equal three. Our main results concern the study of the effect on the expressive power of higher-order logics, of simultaneously bounding the arity of the higher-order variables and the alternation of quantifiers. Let AAi(r,m) be the class of (i + 1)-th order logic formulae where all quantifiers are grouped together at the beginning of the formulae, forming m alternating blocks of consecutive existential and universal quantifiers, and such that the maximal-arity (a generalization of the concept of arity, not just the maximal of the arities of the quantified variables) of the higher-order variables is bounded by r. Note that, the order of the quantifiers in the prefix may be mixed. We show that, for every i [greater than or equal to] 1, the resulting AAi hierarchy of formulae of (i + 1)-th order logic is proper. This extends a result by Makowsky and Pnueli who proved that the same hierarchy in second-order logic is proper. In both cases the strategy used to prove the results consists in considering the set AUTOSAT(F) of formulae in a given logic F which, represented as finite structures, satisfy themselves. We then use a similar strategy to prove that the classes of [Sigma superscript i subscript m union Pi superscript i subscript m] formulae in which the higher-order variables of all orders up to i+1 have maximal-arity at most r, also induce a proper hierarchy in each higher-order logic of order i [greater than or equal to] 3. It is not known whether the correspondent hierarchy in second-order logic is proper. Using the concept of finite model truth definitions introduced by M. Mostowski, we give a sufficient condition for that to be the case. We also study the complexity of the set AUTOSAT(F) and show that when F is one of the prenex fragments [Sigma superscript 1 subscript m] of second-order logic, it follows that AUTOSAT(F) becomes a complete problem for the corresponding prenex fragment [Sigma superscript 2 subscript m] of third-order logic. Finally, aiming to provide the background for a future line of research in higher-order logics, we take a closer look to the restricted second-order logic SO[superscript w] introduced by Dawar. We further investigate its connection with the concept of relational complexity studied by Abiteboul, Vardi and Vianu. Dawar showed that the existential fragment of SO[superscript w] is equivalent to the nondeterministic inflationary fixed-point logic NFP. Since NFP captures relational NP, it follows that the existential fragment of SO[superscript w] captures relational NP. We give a direct proof, in the style of the proof of Fagin’s theorem, of this fact. We then define formally the concept of relational machine with relational oracle and prove the exact correspondence between the prenex fragments of SO[superscript w] and the levels of the relational polynomial-time hierarchy. This allows us to stablish a direct connection between the relational polynomial hierarchy and SO without using the Abiteboul and Vianu normal form for relational machines.

We investigate the expressive power of different fragments of higher-order logics over finite relational structures (or equivalently, relational databases) with special emphasis in higher-order logics of order greater than or equal three. Our main results concern the study of the effect on the expressive power of higher-order logics, of simultaneously bounding the arity of the higher-order variables and the alternation of quantifiers. Let AAi(r,m) be the class of (i + 1)-th order logic formulae where all quantifiers are grouped together at the beginning of the formulae, forming m alternating blocks of consecutive existential and universal quantifiers, and such that the maximal-arity (a generalization of the concept of arity, not just the maximal of the arities of the quantified variables) of the higher-order variables is bounded by r. Note that, the order of the quantifiers in the prefix may be mixed. We show that, for every i [greater than or equal to] 1, the resulting AAi hierarchy of formulae of (i + 1)-th order logic is proper. This extends a result by Makowsky and Pnueli who proved that the same hierarchy in second-order logic is proper. In both cases the strategy used to prove the results consists in considering the set AUTOSAT(F) of formulae in a given logic F which, represented as finite structures, satisfy themselves. We then use a similar strategy to prove that the classes of [Sigma superscript i subscript m union Pi superscript i subscript m] formulae in which the higher-order variables of all orders up to i+1 have maximal-arity at most r, also induce a proper hierarchy in each higher-order logic of order i [greater than or equal to] 3. It is not known whether the correspondent hierarchy in second-order logic is proper. Using the concept of finite model truth definitions introduced by M. Mostowski, we give a sufficient condition for that to be the case. We also study the complexity of the set AUTOSAT(F) and show that when F is one of the prenex fragments [Sigma superscript 1 subscript m] of second-order logic, it follows that AUTOSAT(F) becomes a complete problem for the corresponding prenex fragment [Sigma superscript 2 subscript m] of third-order logic. Finally, aiming to provide the background for a future line of research in higher-order logics, we take a closer look to the restricted second-order logic SO[superscript w] introduced by Dawar. We further investigate its connection with the concept of relational complexity studied by Abiteboul, Vardi and Vianu. Dawar showed that the existential fragment of SO[superscript w] is equivalent to the nondeterministic inflationary fixed-point logic NFP. Since NFP captures relational NP, it follows that the existential fragment of SO[superscript w] captures relational NP. We give a direct proof, in the style of the proof of Fagin’s theorem, of this fact. We then define formally the concept of relational machine with relational oracle and prove the exact correspondence between the prenex fragments of SO[superscript w] and the levels of the relational polynomial-time hierarchy. This allows us to stablish a direct connection between the relational polynomial hierarchy and SO without using the Abiteboul and Vianu normal form for relational machines.

We investigate the expressive power of different fragments of higher-order logics over finite relational structures (or equivalently, relational databases) with special emphasis in higher-order logics of order greater than or equal three. Our main results concern the study of the effect on the expressive power of higher-order logics, of simultaneously bounding the arity of the higher-order variables and the alternation of quantifiers. Let AAi(r,m) be the class of (i + 1)-th order logic formulae where all quantifiers are grouped together at the beginning of the formulae, forming m alternating blocks of consecutive existential and universal quantifiers, and such that the maximal-arity (a generalization of the concept of arity, not just the maximal of the arities of the quantified variables) of the higher-order variables is bounded by r. Note that, the order of the quantifiers in the prefix may be mixed. We show that, for every i [greater than or equal to] 1, the resulting AAi hierarchy of formulae of (i + 1)-th order logic is proper. This extends a result by Makowsky and Pnueli who proved that the same hierarchy in second-order logic is proper. In both cases the strategy used to prove the results consists in considering the set AUTOSAT(F) of formulae in a given logic F which, represented as finite structures, satisfy themselves. We then use a similar strategy to prove that the classes of [Sigma superscript i subscript m union Pi superscript i subscript m] formulae in which the higher-order variables of all orders up to i+1 have maximal-arity at most r, also induce a proper hierarchy in each higher-order logic of order i [greater than or equal to] 3. It is not known whether the correspondent hierarchy in second-order logic is proper. Using the concept of finite model truth definitions introduced by M. Mostowski, we give a sufficient condition for that to be the case. We also study the complexity of the set AUTOSAT(F) and show that when F is one of the prenex fragments [Sigma superscript 1 subscript m] of second-order logic, it follows that AUTOSAT(F) becomes a complete problem for the corresponding prenex fragment [Sigma superscript 2 subscript m] of third-order logic. Finally, aiming to provide the background for a future line of research in higher-order logics, we take a closer look to the restricted second-order logic SO[superscript w] introduced by Dawar. We further investigate its connection with the concept of relational complexity studied by Abiteboul, Vardi and Vianu. Dawar showed that the existential fragment of SO[superscript w] is equivalent to the nondeterministic inflationary fixed-point logic NFP. Since NFP captures relational NP, it follows that the existential fragment of SO[superscript w] captures relational NP. We give a direct proof, in the style of the proof of Fagin’s theorem, of this fact. We then define formally the concept of relational machine with relational oracle and prove the exact correspondence between the prenex fragments of SO[superscript w] and the levels of the relational polynomial-time hierarchy. This allows us to stablish a direct connection between the relational polynomial hierarchy and SO without using the Abiteboul and Vianu normal form for relational machines.

The quality of Machine Translation (MT) can often be poor due to it appearing incoherent and lacking in fluency. These problems consist of word ordering, awkward use of words and grammar, and translating text too literally. However we should not consider translations such as these failures until we have done our best to enhance their quality, or more simply, their fluency. In the same way various processes can be applied to touch up a photograph, various processes can also be applied to touch up a translation. This research outlines the improvement of MT quality through the application of Fluency Enhancement (FE), which is a process we have created that reforms and evaluates text to enhance its fluency. We have tested our FE process on our own MT system which operates on what we call the SAM fundamentals, which are as follows: Simplicity - to be simple in design in order to be portable across different languages pairs, Adaptability - to compensate for the evolution of language, and Multiplicity - to determine a final set of translations from as many candidate translations as possible. Based on our research, the SAM fundamentals are the key to developing a successful MT system, and are what have piloted the success of our FE process.