The School of Informatics brings together research in Computer Science, Cognitive Science, Computational Linguistics and Artificial Intelligence. It provides a fertile environment for a wide range of interdisciplinary studies, leading to this new science of Informatics.

Recent Submissions

  • Infandango: Automated Grading for Student Programming 

    Hull, Michael; Powell, Dan; Klein, Ewan (Association for Computing Machinery, 2011-06)
    Infandango is an open source web-based system for automated grading of Java code submitted by students. Uploaded Java files are compiled and run against a set of unit tests on a central server, with results being stored ...
  • The Romanian Speech Synthesis (RSS) corpus: building a high quality HMM-based speech synthesis system using a high sampling rate 

    Stan, Adriana; Yamagishi, Junichi; King, Simon; Aylett, Matthew (Elsevier, 2011-03)
    This paper first introduces a newly-recorded high quality Romanian speech corpus designed for speech synthesis, called “RSS”, along with Romanian front-end text processing modules and HMM-based synthetic voices built from ...
  • Speaker similarity evaluation of foreign-accented speech synthesis using HMM-based speaker adaptation 

    Wester, Mirjam; Karhila, Reima (IEEE, 2011-05)
    This paper describes a speaker discrimination experiment in which native English listeners were presented with natural and synthetic speech stimuli in English and were asked to judge whether they thought the sentences were ...
  • Roles of the Average Voice in Speaker-adaptive HMM-based Speech Synthesis 

    Yamagishi, Junichi; Watts, Oliver; King, Simon; Usabaev, Bela (ISCA, 2010)
    In speaker-adaptive HMM-based speech synthesis, there are a few speakers whose synthetic speech sounds worse than that of other speakers, despite having the same amount of adaptation data from within the same corpus. This ...
  • The CSTR/EMIME HTS system for Blizzard Challenge 2010 

    Yamagishi, Junichi; Watts, Oliver (2010)
    In the 2010 Blizzard Challenge, we focused on improving steps relating to feature extraction and labeling in the procedures for training HMM-based speech synthesis systems. New auditory scales were used for spectral ...
  • Vocal Attractiveness Of Statistical Speech Synthesisers 

    Andraszewicz, Sandra; Yamagishi, Junichi; King, Simon (IEEE, 2011)
    Our previous analysis of speaker-adaptive HMM-based speech synthesis methods suggested that there are two possible reasons why average voices can obtain higher subjective scores than any individual adapted voice: 1) model ...
  • The EMIME Mandarin Bilingual Database 

    Wester, Mirjam; Liang, Hui (The University of Edinburgh, 2011)
    This paper describes the collection of a bilingual database of Mandarin/English data. In addition, the accents of the talkers in the database have been rated. English and Mandarin listeners assessed the English and Mandarin ...
  • The EMIME Bilingual Database 

    Wester, Mirjam (The University of Edinburgh, 2010)
    This paper describes the collection of a bilingual database of Finnish/English and German/English data. In addition, the accents of the talkers in the database have been rated. English, German and Finnish listeners assessed ...
  • Place memory in crickets 

    Wessnitzer, J.; Mangan, M.; Webb, B. (2008)
  • Verified Planning by Deductive Synthesis in Intuitionistic Linear Logic 

    Dixon, L.; Bundy, Alan; Smaill, A. (2009)
    We describe a new formalisation in Isabelle/HOL of Intuitionistic Linear Logic and consider the support this provides for constructing plans by proving the achievability of given planning goals. The plans so found are ...
  • A Small Experiement in Event-b Rippling 

    Grov, Gudmund,; Bundy, Alan; Dixon, Lucas (2011-02-03)
  • Dynamic Rippling, Middle-Out Reasoning and Lemma Discovery 

    Johansson, Moa; Dixon, Lucas; Bundy, Alan (Springer-Verlag, 2010)
    We present a succinct account of dynamic rippling, a technique used to guide the automation of inductive proofs. This simplifies termination proofs for rippling and hence facilitates extending the technique in ways that ...
  • Isacosy: Synthesis of Inductive Theorems 

    Dixon, Lucas; Bundy, Alan; Johansson, Moa (2009)
    We have implemented a program for inductive theory formation, called IsaCoSy, which synthesises conjectures about recursively defined datatypes and functions. Only irreducible terms are generated, which keeps the search ...
  • A Single-Significant-Digit Calculus for Semi-Automated Guesstimation 

    Abourbih, J.A.; Blaney, L.; Bundy, Alan; McNeill, F. (SpringerLink, 2010)
    We describe a single-significant-digit calculus for estimating approximate solutions to guesstimation problems. The calculus is formalised as a collection of proof methods, which are combined into proof plans. These proof ...
  • Rippling: A Heuristic for Guiding Inductive Proofs 

    Bundy, Alan; Stevens, A.; van Harmelen, F.; Ireland, A.; Smaill, A. (Elsevier, 1993-08)
    We describe rippling: a tactic for the heuristic control of the key part of proofs by mathematical induction. This tactic significantly reduces the search for a proof of a wide variety of inductive theorems. We first present ...
  • Conjecture Synthesis for Inductive Theories 

    Johansson, Moa; Dixon, Lucas; Bundy, Alan (SpringerLink, 2010)
    We have developed a program for inductive theory formation, called IsaCoSy, which synthesises conjectures ‘bottom-up’ from the available constants and free variables. The synthesis process is made tractable by only generating ...
  • Formalising Term Synthesis for Isacosy 

    Johansson, Moa; Dixon, Lucas; Bundy, Alan (2010)
    IsaCoSy is a theory formation system for inductive theories. It synthesises conjectures and uses the ones that can be proved to produce a background theory for a new formalisation within a proof assistant. We present a ...
  • Qualitative Causal Analysis of Empirical Knowledge for Ontology Evolution in Physics 

    Lehmann, J.; Bundy, Alan; Chan, M. (2010-08-16)
    Ontology evolution and its automation are key factors for achieving software’s flexibility and adaptability. In the approach to automated ontology evolution adopted in the GALILEO project, progress in physics is modelled ...
  • Calculating Criticalities 

    Alan, Bundy; Giunchiglia, F.; Sebastiani, R.; Walsh, T. (Elsevier, 1996-12)
    We present a novel method for building style abstraction hierarchies in planning. The aim of this method is to minimize search by limiting backtracking both between abstraction levels and within an abstraction level. ...

View more