Now showing items 1-20 of 53

  • Robot dynamics algorithms 

    Featherstone, Roy (The University of Edinburgh, 1984)
    In this dissertation I introduce a new notation for representing rigid-body dynamics, and use it to describe a number of methods for calculating robot dynamics efficiently. The notation (called spatial notation) is based ...
  • The Polyadic pi-Calculus: A Tutorial 

    Milner, Robin (The University of Edinburgh, 1991)
    The pi-calculus is a model of concurrent computation based upon the notion of naming. It is first presented in its simplest and original form, with the help of several illustrative applications. Then it is generalized from ...
  • Computational mechanisms for action selection 

    Tyrrell, Toby (The University of Edinburgh, 1993)
    Imagine a zebra in the African savannah. At each moment in time this zebra has to weigh up alternative courses of action before deciding which will be most beneficial to it. For instance, it may want to graze because it ...
  • Making a Productive Use of Failure to Generate Witnesses for Coinduction from Divergent Proof Attempts 

    Dennis, Louise; Bundy, Alan; Green, Ian (1999)
    Coinduction is a proof rule. It is the dual of induction. It allows reasoning about non--well--founded structures such as lazy lists or streams and is of particular use for reasoning about equivalences. A central difficulty ...
  • Developing the Incongruity-Resolution Theory 

    Ritchie, Graeme (1999-04)
    The idea of incongruity-resolution has frequently been suggested as an account of many types of joke. However, there is no precise statement either of this ``theory'' nor of its main concepts (incongruity and resolution), ...
  • The Automation Of Proof By Mathematical Induction 

    Bundy, Alan (1999-04)
    This paper is a chapter of the Handbook of Automated Reasoning edited by Voronkov and Robinson. It describes techniques for automated reasoning in theories containing rules of mathematical induction. Firstly, inductive ...
  • A Survey of Automated Deduction 

    Bundy, Alan (1999-04)
    We survey research in the automation of deductive inference, from its beginnings in the early history of computing to the present day. We identify and describe the major areas of research interest and their applications. ...
  • Proofs About Lists Using Ellipsis 

    Bundy, Alan; Richardson, Julian (1999-09)
    In this paper we explore the use of ellipsis in proofs about lists. We present a higher-order formulation of elliptic formulae, and describe its implementation in the LambdaClam proof planner. We use an unambiguous ...
  • Using AI Planning Techniques for Army Small Unit Operations 

    Tate, Austin; Levine, John; Jarvis, Peter; Dalton, Jeffrey (1999-12)
    In this paper, we outline the requirements of a planning and decision aid to support US Army small unit operations in urban terrain and show how AI planning technologies can be exploited in that context. The work is a rare ...
  • Animal learning models as robot controllers 

    Hallam, Bridget (The University of Edinburgh, 2000)
    Robots can do a range of wonderful things, but they can also appear really stupid. I would like my autonomous, sensor-rich, robot to be able to: complete its task whenever possible, despite distractions and disabilities; ...
  • Completeness Conditions for Mixed Strategy Bidirectional Parsing 

    Ritchie, Graeme (The University of Edinburgh, 2000)
    It has been suggested that, in certain circumstances, it might be useful for a grammar-writer to annotate which rules are to be used bottom-up and which are to be used top-down within a parser, using a bidirectional variant ...
  • Towards A Computational Model Of Poetry Generation 

    Manurung, Hisar; Ritchie, Graeme; Thompson, Henry (The University of Edinburgh, 2000)
    In this paper we describe the difficulties of poetry generation, particularly in contrast to traditional informative natural language generation. We then point out deficiencies of previous attempts at poetry generation, ...
  • The Direct Route: Mediated Priming in Semantic Space 

    Lowe, Will; McDonald, Scott (The University of Edinburgh, 2000)
    McKoon and Ratcliff (1992) presented a theory of mediated priming where the priming effect is due to a direct but weak relatedness between prime and target. They also introduced a quantitative measure of word relatedness ...
  • A Web Based Replayer For Proof General 

    Freear, Jonathan (The University of Edinburgh, 2000)
    Proof General is a generic interface for proof assistants, based on Emacs. It has been developed at the LFCS in the University of Edinburgh. One of the nice features of Proof General is that it is very easy to replay ...
  • Cross Domain Mathematical Concept Formation 

    Steel, Graham; Colton, Simon; Bundy, Alan; Walsh, Toby (The University of Edinburgh, 2000)
    Many interesting concepts in mathematics are essentially "cross-domain" in nature, relating objects from more than one area of mathematics, e.g. prime order groups. These concepts are often vital to the formation of a ...
  • Resolving References to Graphical Objects in Multimodal Queries by Constraint Satisfaction 

    He, Daqing; Ritchie, Graeme; Lee, John (The University of Edinburgh, 2000)
    In natural language queries to an intelligent multimodal system, ambiguities related to referring expressions -- source ambiguities -- can occur between items in the visual display and objects in the domain being represented. ...
  • Design and Implementation of an Online Auction 

    Theodoropoulos, Theodoros (The University of Edinburgh, 2000)
    This dissertation reports on the design and implementation of a distributed application that hosts online auctions. The system is implemented using Java and CORBA. Special care has been taken to make it secure, flexible, ...
  • Frame: An Imperative Coordination Language for Parallel Programming 

    Cole, Murray (The University of Edinburgh, 2000)
    We present Frame, a simple language which facilitates structured expression of imperative parallelism. Programs are described at two levels. The top level captures the main parallel algorithmic structure (which may be ...
  • Formal Support for an Informal Business Modelling Method 

    Chen-Burger, Jessica; Robertson, Dave; Stader, Justine (The University of Edinburgh, 2000)
    Business modelling methods are popular but, since they operate primarily in the early stages of software lifecycles, most are informal. This paper describes how we have used a conventional formal notation (first order ...
  • Isamode: Theorem Proving with Isabelle inside Emacs 

    Aspinall, David (The University of Edinburgh, 2000)
    This paper documents Isamode, a user-interface and suite of editing functions for using the theorem prover Isabelle inside Emacs.