Logic of Violations: A gentzen systems for reasoning with contrary-to-duty obligations

In this paper we present a Gentzen system for reasoning with contrary-to-duty obligations. The intuition behind the system is that a contrary-to-duty is a special kind of normative exception. The logical machinery to formalise this idea is taken from substructural logics and it is based on the definition of a new non-classical connective capturing the notion of reparational obligation. Then the system is tested against well-known contrary-to-duty paradoxes.

Linear temporal logic and z refinement

Since Z, being a state-based language, describes a system in terms of its state and potential state changes, it is natural to want to describe properties of a specified system also in terms of its state. One means of doing this is to use Linear Temporal Logic (LTL) in which properties about the state of a system over time can be captured. This, however, raises the question of whether these properties are preserved under refinement. Refinement is observation preserving and the state of a specified system is regarded as internal and, hence, non-observable. In this paper, we investigate this issue by addressing the following questions. Given that a Z specification A is refined by a Z specification C, and that P is a temporal logic property which holds for A, what temporal logic property Q can we deduce holds for C? Furthermore, under what circumstances does the property Q preserve the intended meaning of the property P? The paper answers these questions for LTL, but the approach could also be applied to other temporal logics over states such as CTL and the mgr-calculus.

Applications of the Jameson cell at the head of base metal flotation circuits

The Jameson Cell is a high intensity flotation device, which utilises induced air from the atmosphere. It was developed jointly by Mount Isa Mines and Professor Graeme Jameson of the University of Newcastle in the 1980s. It is proven to generate fine bubbles, in the order of 300 to 500 µm, in a high intensity, high shear and compact zone contained in the downcomer. This aerated mixture exits the downcomer into the pulp zone, which is the quiescent mineral and gangue separation zone. A number of Australian base metal flotation circuits feature a reverse flotation stage at the head of the circuit. Testwork and plant operating data has shown that the use of a Jameson Cell in the prefloat cleaner application has further improved prefloat gangue recovery and selectivity. Operation of a Jameson Cell in a carbonaceous/pyrite prefloat cleaner duty at the Mt Isa copper concentrator increased copper recovery and reduced pyrite in the copper concentrate. Testwork at Zinifex Century Zinc Mine showed a decrease in zinc losses by the utilisation of Jameson Cell prefloat cleaner. Appraisal of a Jameson Cell in a scalping role within the Mt Isa Copper Concentrator indicated significant benefits could be achieved.

Norm modifications in defeasible logic

This paper proposes a framework based on Defeasible Logic (DL) to reason about normative modifications. We show how to express them in DL and how the logic deals with conflicts between temporalised normative modifications. Some comments will be given with regard to the phenomenon of retroactivity.

A technique for modular logic program refinement

A refinement calculus provides a method for transforming specifications to executable code, maintaining the correctness of the code with respect to its specification. In this paper we introduce modules into a logic programming refinement calculus. Modules allow data types to be grouped together with sets of procedures that manipulate the data types. By placing restrictions on the way a program uses a module, we develop a technique for refining the module so that it uses a more efficient representation of the data type.