Browsing Informatics Report Series by Issue Date
Now showing items 120 of 53

Robot dynamics algorithms
(The University of Edinburgh, 1984)In this dissertation I introduce a new notation for representing rigidbody dynamics, and use it to describe a number of methods for calculating robot dynamics efficiently. The notation (called spatial notation) is based ... 
The Polyadic piCalculus: A Tutorial
(The University of Edinburgh, 1991)The picalculus 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
(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
(1999)Coinduction is a proof rule. It is the dual of induction. It allows reasoning about nonwellfounded structures such as lazy lists or streams and is of particular use for reasoning about equivalences. A central difficulty ... 
Developing the IncongruityResolution Theory
(199904)The idea of incongruityresolution 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
(199904)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
(199904)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
(199909)In this paper we explore the use of ellipsis in proofs about lists. We present a higherorder 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
(199912)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
(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, sensorrich, robot to be able to: complete its task whenever possible, despite distractions and disabilities; ... 
Completeness Conditions for Mixed Strategy Bidirectional Parsing
(The University of Edinburgh, 2000)It has been suggested that, in certain circumstances, it might be useful for a grammarwriter to annotate which rules are to be used bottomup and which are to be used topdown within a parser, using a bidirectional variant ... 
Towards A Computational Model Of Poetry Generation
(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
(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
(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
(The University of Edinburgh, 2000)Many interesting concepts in mathematics are essentially "crossdomain" 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
(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
(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
(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
(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
(The University of Edinburgh, 2000)This paper documents Isamode, a userinterface and suite of editing functions for using the theorem prover Isabelle inside Emacs.