On the comparison of proof planning systems: Lambda-clam, Omega and IsaPlanner

We present a framework for describing proof planners. This framework is based around a decomposition of proof planners into planning states, proof language, proof plans, proof methods, proof revision, proof control and planning algorithms. We use this framework to motivate the comparison of three recent proof planning systems, lclam, OMEGA and IsaPlanner, and demonstrate how the framework allows us to discuss and illustrate both their similarities and differences in a consistent fashion. This analysis reveals that proof control and the use of contextual information in planning states are key areas in need of further investigation.

Inductive Theorem Proving and Computer Algebra in the Mathweb Software Bus

Reasoning systems have reached a high degree of maturity in the last decade. However, even the most successful systems are usually not general purpose problem solvers but are typically specialised on problems in a certain domain. The MathWeb SOftware Bus (Mathweb-SB) is a system for combining reasoning specialists via a common osftware bus. We described the integration of the lambda-clam systems, a reasoning specialist for proofs by induction, into the MathWeb-SB. Due to this integration, lambda-clam now offers its theorem proving expertise to other systems in the MathWeb-SB. On the other hand, lambda-clam can use the services of any reasoning specialist already integrated. We focus on the latter and describe first experimnents on proving theorems by induction using the computational power of the MAPLE system within lambda-clam.

Avian flu: the creation of expectations in the interplay between science and the media

This paper examines the emerging cultural patterns and interpretative repertoires in reports of an impending pandemic of avian flu in the UK mass media and scientific journals at the beginning of 2005, paying particular attention to metaphors, pragmatic markers ('risk signals'), symbolic dates and scare statistics used by scientists and the media to create expectations and elicit actions. This study complements other work on the metaphorical framing of infectious disease, such as foot and mouth disease and SARS, tries to link it to developments in the sociology of expectations and applies insights from pragmatics both to the sociology of metaphor and the sociology of expectations.

Compounds, creativity and complexity in climate change communication: the case of ‘carbon indulgences’

This article deals with climate change from a linguistic perspective. Climate change is an extremely complex issue that has exercised the minds of experts and policy makers with renewed urgency in recent years. It has prompted an explosion of writing in the media, on the internet and in the domain of popular science and literature, as well as a proliferation of new compounds around the word ‘carbon’ as a hub, such as ‘carbon indulgence’, a new compound that will be studied in this article. Through a linguistic analysis of lexical and discourse formations around such ‘carbon compounds’ we aim to contribute to a broader understanding of the meaning of climate change. Lexical carbon compounds are used here as indicators for observing how human symbolic cultures change and adapt in response to environmental threats and how symbolic innovation and transmission occurs.

Discontinuous Galerkin Computation of the Maxwell Eigenvalues on Simplicial Meshes

This paper is concerned with the discontinuous Galerkin approximation of the Maxwell eigenproblem. After reviewing the theory developed in [5], we present a set of numerical experiments which both validate the theory, and provide further insight regarding the practical performance of discontinuous Galerkin methods, particularly in the case when non-conforming meshes, characterized by the presence of hanging nodes, are employed.

The MUSE Machine -- an Architecture for Structured Data Flow Computation

Computers employing some degree of data flow organisation are now well established as providing a possible vehicle for concurrent computation. Although data-driven computation frees the architecture from the constraints of the single program counter, processor and global memory, inherent in the classic von Neumann computer, there can still be problems with the unconstrained generation of fresh result tokens if a pure data flow approach is adopted. The advantages of allowing serial processing for those parts of a program which are inherently serial, and of permitting a demand-driven, as well as data-driven, mode of operation are identified and described. The MUSE machine described here is a structured architecture supporting both serial and parallel processing which allows the abstract structure of a program to be mapped onto the machine in a logical way.