Axiomatisation of an Interval Calculus for Theorem Proving

We provide an axiomatisation of the Timed Interval Calculus, a set-theoretic notation for expressing properties of time intervals. We implement the axiomatisation in the Ergo theorem prover in order to allow the machine-checked proof of laws for reasoning about predicates expressed using interval operators. These laws can be then used in the machine-assisted verification of real-time applications.

Supporting contexts in program refinement

A program can be refined either by transforming the whole program or by refining one of its components. The refinement of a component is, for the main part, independent of the remainder of the program. However, refinement of a component can depend on the context of the component for information about the variables that are in scope and what their types are. The refinement can also take advantage of additional information, such as any precondition the component can assume. The aim of this paper is to introduce a technique, which we call program window inference, to handle such contextual information during derivations in the refinement calculus. The idea is borrowed from a technique, called window inference, for handling context in theorem proving. Window inference is the primary proof paradigm of the Ergo proof editor. This tool has been extended to mechanize refinement using program window inference. (C) 1997 Elsevier Science B.V.

Agent-based distributed software verification

Despite decades of research, the takeup of formal methods for developing provably correct software in industry remains slow. One reason for this is the high cost of proof construction, an activity that, due to the complexity of the required proofs, is typically carried out using interactive theorem provers. In this paper we propose an agent-oriented architecture for interactive theorem proving with the aim of reducing the user interactions (and thus the cost) of constructing software verification proofs. We describe a prototype implementation of our architecture and discuss its application to a small, but non-trivial case study.

Integrating runtime assertions with dynamic types: Structuring a derivation from an incomputable specification

An inherent incomputability in the specification of a functional language extension that combines assertions with dynamic type checking is isolated in an explicit derivation from mathematical specifications. The combination of types and assertions (into "dynamic assertion-types" - DATs) is a significant issue since, because the two are congruent means for program correctness, benefit arises from their better integration in contrast to the harm resulting from their unnecessary separation. However, projecting the "set membership" view of assertion-checking into dynamic types results in some incomputable combinations. Refinement of the specification of DAT checking into an implementation by rigorous application of mathematical identities becomes feasible through the addition of a "best-approximate" pseudo-equality that isolates the incomputable component of the specification. This formal treatment leads to an improved, more maintainable outcome with further development potential.

On the Jager-Kaul theorem concerning harmonic maps

In 1983, Jager and Kaul proved that the equator map u*(x) = (x/\x\,0) : B-n --> S-n is unstable for 3 less than or equal to n less than or equal to 6 and a minimizer for the energy functional E(u, B-n) = integral B-n \del u\(2) dx in the class H-1,H-2(B-n, S-n) with u = u* on partial derivative B-n when n greater than or equal to 7. In this paper, we give a new and elementary proof of this Jager-Kaul result. We also generalize the Jager-Kaul result to the case of p-harmonic maps.

Multifidus muscle recovery is not automatic after resolution of acute, first-episode low back pain

Study Design. A clinical study was conducted on 39 patients with acute, first-episode, unilateral low back pain and unilateral, segmental inhibition of the multifidus muscle. Patients were allocated randomly to a control or treatment group. Objectives. To document the natural course of lumbar multifidus recovery and to evaluate the effectiveness of specific, localized, exercise therapy on muscle recovery. Summary of Background Data. Acute low back pain usually resolves spontaneously, but the recurrence rate is high. Inhibition of multifidus occurs with acute, first-episode, low back pain, and pathologic changes in this muscle have been linked with poor outcome and recurrence of symptoms. Methods. Patients in group 1 received medical treatment only. Patients in group 2 received medical treatment and specific, localized, exercise therapy. Outcome measures for both groups included 4 weekly assessments of pain, disability, range of motion, and size of the multifidus cross-sectional area. Independent examiners were blinded to group allocation. Patients were reassessed at a 10-week follow-up examination. Results. Multifidus muscle recovery was not spontaneous on remission of painful symptoms in patients in group 1. Muscle recovery was more rapid and more complete in patients in group 2 who received exercise therapy (P = 0.0001). Other outcome measurements were similar for the two groups at the 4-week examination. Although they resumed normal levels of activity, patients in group 1 still had decreased multifidus muscle size at the 10-week follow-up examination. Conclusions. Multifidus muscle recovery is not spontaneous on remission of painful symptoms. Lack of localized, muscle support may be one reason for the high recurrence rate of low back pain following the initial episode.

Proving Temporal Properties of Z Specifications Using Abstraction

This paper presents a systematic approach to proving temporal properties of arbitrary Z specifications. The approach involves (i) transforming the Z specification to an abstract temporal structure (or state transition system), (ii) applying a model checker to the temporal structure, (iii) determining whether the temporal structure is too abstract based on the model checking result and (iv) refining the temporal structure where necessary. The approach is based on existing work from the model checking literature, adapting it to Z.

A fuzzy max-flow min-cut theorem

Interval-valued versions of the max-flow min-cut theorem and Karp-Edmonds algorithm are developed and provide robustness estimates for flows in networks in an imprecise or uncertain environment. These results are extended to networks with fuzzy capacities and flows. (C) 2001 Elsevier Science B.V. All rights reserved.

A flux ratio theorem for multicomponent linear diffusion equations

Ussing [1] considered the steady flux of a single chemical component diffusing through a membrane under the influence of chemical potentials and derived from his linear model, an expression for the ratio of this flux and that of the complementary experiment in which the boundary conditions were interchanged. Here, an extension of Ussing's flux ratio theorem is obtained for n chemically interacting components governed by a linear system of diffusion-migration equations that may also incorporate linear temporary trapping reactions. The determinants of the output flux matrices for complementary experiments are shown to satisfy an Ussing flux ratio formula for steady state conditions of the same form as for the well-known one-component case. (C) 2000 Elsevier Science Ltd. All rights reserved.

Semantic priming in Alzheimer's dementia: Evidence for dissociation of automatic and attentional processes

The nature of the semantic memory deficit in dementia of the Alzheimer's type (DAT) was investigated in a semantic priming task which was designed to assess both automatic and attention-induced priming effects. Ten DAT patients and 10 age-matched control subjects completed a word naming semantic priming task in which both relatedness proportion (RP) and stimulus-onset asynchrony (SOA) were varied. A clear dissociation between automatic and attentional priming effects in both groups was demonstrated; however, the DAT subjects pattern of priming deviated significantly from that of the normal controls. The DAT patients failed to produce any priming under conditions which encouraged automatic semantic processing and produced facilitation only when the RP was high. In addition, the DAT group produced hyperpriming, with significantly larger facilitation effects than the control group. These results suggest an impairment of automatic spreading activation in DAT and have implications for theories of semantic memory impairment in DAT as well as models of normal priming. (C) 2001 Academic Press.

On a theorem of Cooper

In this paper we study some purely mathematical considerations that arise in a paper of Cooper on the foundations of thermodynamics that was published in this journal. Connections with mathematical utility theory are studied and some errors in Cooper's paper are rectified. (C) 2001 Academic Press.

Thue's theorem and the diophantine equation x2 - Dy2 = ±N

A constructive version of a theorem of Thue is used to provide representations of certain integers as x(2) - Dy-2, where D = 2, 3, 5, 6, 7.

Automatic construction of explicit R matrices for the one-parameter families of irreducible typical highest weight (0(m)vertical bar alpha(n)) representations of U-q[gl(m vertical bar n)]

We detail the automatic construction of R matrices corresponding to (the tensor products of) the (O-m\alpha(n)) families of highest-weight representations of the quantum superalgebras Uq[gl(m\n)]. These representations are irreducible, contain a free complex parameter a, and are 2(mn)-dimensional. Our R matrices are actually (sparse) rank 4 tensors, containing a total of 2(4mn) components, each of which is in general an algebraic expression in the two complex variables q and a. Although the constructions are straightforward, we describe them in full here, to fill a perceived gap in the literature. As the algorithms are generally impracticable for manual calculation, we have implemented the entire process in MATHEMATICA; illustrating our results with U-q [gl(3\1)]. (C) 2002 Published by Elsevier Science B.V.

Stereological and other methods applied to rock joint size estimation - Does Crofton's theorem apply?

A number of authors concerned with the analysis of rock jointing have used the idea that the joint areal or diametral distribution can be linked to the trace length distribution through a theorem attributed to Crofton. This brief paper seeks to demonstrate why Crofton's theorem need not be used to link moments of the trace length distribution captured by scan line or areal mapping to the moments of the diametral distribution of joints represented as disks and that it is incorrect to do so. The valid relationships for areal or scan line mapping between all the moments of the trace length distribution and those of the joint size distribution for joints modeled as disks are recalled and compared with those that might be applied were Crofton's theorem assumed to apply. For areal mapping, the relationship is fortuitously correct but incorrect for scan line mapping.