Temporal reasoning about action and change

Abstract not available

A discrete formalism for reasoning about action and change

This paper presents a discrete formalism for temporal reasoning about actions and change, which enjoys an explicit representation of time and action/event occurrences. The formalism allows the expression of truth values for given fluents over various times including nondecomposable points/moments and decomposable intervals. Two major problems which beset most existing interval-based theories of action and change, i.e., the so-called dividing instant problem and the intermingling problem, are absent from this new formalism. The dividing instant problem is overcome by excluding the concepts of ending points of intervals, and the intermingling problem is bypassed by means of characterising the fundamental time structure as a well-ordered discrete set of non-decomposable times (points and moments), from which decomposable intervals are constructed. A comprehensive characterisation about the relationship between the negation of fluents and the negation of involved sentences is formally provided. The formalism provides a flexible expression of temporal relationships between effects and their causal events, including delayed effects of events which remains a problematic question in most existing theories about action and change.

Reasoning about change over time: Actions, events and their effects

This paper presents a new formalism for reasoning about change over time. The formalism derives a clean separation between the notion of states and situations. It allows more flexible temporal causal relationships than do other formalisms for reasoning about causal change, such as the situation calculus and the event calculus. It includes effects that start during, immediately after, or some time after their causes, and which end before, simultaneously with, or after their causes. A formal distinction between actions, action-types and events is proposed, which allows the expression of common-sense causal laws at high level. It is shown how these laws can be used to deduce state change over time at low level, when events occur under certain preconditions hold. Two problems that beset most interval-based temporal systems, i.e., the so-called dividing instant problem and intermingling problem, are absent from the formalism.

Evaluating the effectiveness of Z: The claims made about CICS and where we go from here

There have been few genuine success stories about industrial use of formal methods. Perhaps the best known and most celebrated is the use of Z by IBM (in collaboration with Oxford University's Programming Research Group) during the development of CICS/ESA (version 3.1). This work was rewarded with the prestigious Queen's Award for Technological Achievement in 1992 and is especially notable for two reasons: 1) because it is a commercial, rather than safety- or security-critical, system and 2) because the claims made about the effectiveness of Z are quantitative as well as qualitative. The most widely publicized claims are: less than half the normal number of customer-reported errors and a 9% savings in the total development costs of the release. This paper provides an independent assessment of the effectiveness of using Z on CICS based on the set of public domain documents. Using this evidence, we believe that the case study was important and valuable, but that the quantitative claims have not been substantiated. The intellectual arguments and rationale for formal methods are attractive, but their widespread commercial use is ultimately dependent upon more convincing quantitative demonstrations of effectiveness. Despite the pioneering efforts of IBM and PRG, there is still a need for rigorous, measurement-based case studies to assess when and how the methods are most effective. We describe how future similar case studies could be improved so that the results are more rigorous and conclusive.

Writing about war: Jung, Much Ado About Nothing, and the Troy novels of Lindsay Clarke

Arguably, in a time of war literature, and indeed all writing, is saturated with deep psychic responses to conflict. So that not only in literary genres such as epic and tragedy, but also in the novel and comedy, can writing about war be discerned. C.G. Jung, Shakespeare and Lindsay Clarke are fundamentally writers of war who share allied literary strategies. Moreover, they diagnose similar origins to the malaise of a culture tending to war in the neglect of aspects of the feminine that patriarchy prefers to ignore. In repressing or evading the dark feminine, cultures as dissimilar as ancient Greece, the 21st century, Shakespeare's England and Jung's Europe prevent the healing energies of the conjunctio of masculine and feminine from stabilising an increasingly fragile consciousness. In the Troy novels of Clarke, Answer to Job by Jung and Much Ado About Nothing by Shakespeare, some attempt at spiritual nourishment is made through the writing. [From the Publisher]

Sex talk? overcoming barriers about sex and contraception after childbirth

Anecdotal evidence tells professionals that childbirth is the best form of contraception. However, sexual health problems are the very common after childbirth with Barrett et al (2000) arguing that only 15% of women who have a postnatal sexual problem reported discussing it with a health professional. As health professionals with a predilection for the ‘clinical’ and the ‘prescriptive’ we organise antenatal classes to discuss bathing the baby and post partum reunions to recount birth stories, but often fail to address sexual health problems and contraception after birth.(Glazener 1997). Many women who have carefully used contraception for years prior to pregnancy are often not helped to re-engage with the issues following birth. This would seem to be a particular problem for the most vulnerable parents such as adolescent mothers and their partners (Social Exclusion Unit 1999, 2004) where some young women go on to have more than one baby in a short time period (Reeves 2003). The focus of this paper is to explore the apparent general failure of health professionals to discuss sex after childbirth and provide information regarding reliable contraception. Glazener (1997) tells us that health professionals are encouraged to educate and prepare patients antenatally, for example to be trained to identify problems and deal with them openly and sympathetically. What is brought into question is why this form of rigorous support is not extended to providing sexual health advice in the immediate and often vulnerable postnatal period and why this provision is not a priority for some groups. The paper will explore if this situation caused by a lack of training or is it a symptom of our culture and a British attitude towards sex and contraception.

A reified temporal logic

This paper presents a reified temporal logic for representing and reasoning about temporal and non-temporal relationships between non-temporal assertions. A clear syntax and semantics for the logic is formally provided. Three types of predicates, temporal predicates, non-temporal predicates and meta-predicates, are introduced. Terms of the proposed language are partitioned into three types, temporal terms, non-temporal terms and propositional terms. Reified propositions consist of formulae with each predicate being either a temporal predicate or a meta-predicate. Meta-predicates may take both temporal terms and propositional terms together as arguments or take propositional terms alone. A standard formula of the classical first-order language with each predicate being a non-temporal predicate taking only non-temporal terms as arguments is reified as just a propositional term. A general time ontology has been provided which can be specialized to a variety of existing temporal systems. The new logic allows one to predicate and quantify over propositional terms while according a special status of time; for example, assertions such as ‘effects cannot precede their causes’ is ensured in the logic, and some problematic temporal aspects including the delay time between events and their effects can be conveniently expressed. Applications of the logic are presented including the characterization of the negation of properties and their contextual sentences, and the expression of temporal relations between actions and effects.