Monodic temporal resolution

Until recently, First-Order Temporal Logic (FOTL) has been only partially understood. While it is well known that the full logic has no finite axiomatisation, a more detailed analysis of fragments of the logic was not previously available. However, a breakthrough by Hodkinson et al., identifying a finitely axiomatisable fragment, termed the monodic fragment, has led to improved understanding of FOTL. Yet, in order to utilise these theoretical advances, it is important to have appropriate proof techniques for this monodic fragment.In this paper, we modify and extend the clausal temporal resolution technique, originally developed for propositional temporal logics, to enable its use in such monodic fragments. We develop a specific normal form for monodic formulae in FOTL, and provide a complete resolution calculus for formulae in this form. Not only is this clausal resolution technique useful as a practical proof technique for certain monodic classes, but the use of this approach provides us with increased understanding of the monodic fragment. In particular, we here show how several features of monodic FOTL can be established as corollaries of the completeness result for the clausal temporal resolution method. These include definitions of new decidable monodic classes, simplification of existing monodic classes by reductions, and completeness of clausal temporal resolution in the case of monodic logics with expanding domains, a case with much significance in both theory and practice.

Mechanising first-order temporal resolution

First-order temporal logic is a concise and powerful notation, with many potential applications in both Computer Science and Artificial Intelligence. While the full logic is highly complex, recent work on monodic first-order temporal logics has identified important enumerable and even decidable fragments. Although a complete and correct resolution-style calculus has already been suggested for this specific fragment, this calculus involves constructions too complex to be of practical value. In this paper, we develop a machine-oriented clausal resolution method which features radically simplified proof search. We first define a normal form for monodic formulae and then introduce a novel resolution calculus that can be applied to formulae in this normal form. By careful encoding, parts of the calculus can be implemented using classical first-order resolution and can, thus, be efficiently implemented. We prove correctness and completeness results for the calculus and illustrate it on a comprehensive example. An implementation of the method is briefly discussed.

Monodic Temporal Resolution

First-order temporal logic is a coincise and powerful notation, with many potential applications in both Computer Science and Artificial Intelligence. While the full logic is highly complex, recent work on monodic first-order temporal logics have identified important enumerable and even decidable fragments. In this paper we present the first resolution-based calculus for monodic first-order temporal logic. Although the main focus of the paper is on establishing completeness result, we also consider implementation issues and define a basic loop-search algorithm that may be used to guide the temporal resolution system.

Stratified resolution

We introduce a calculus of stratified resolution, in which special attention is paid to clauses that "define" relations. If such clauses are discovered in the initial set of clauses, they are treated using the rule of definition unfolding, i.e. the rule that replaces defined relations by their definitions. Stratified resolution comes with a powerful notion of redundancy: a clause to which definition unfolding has been applied can be removed from the search space. To prove the completeness of stratified resolution with redundancies, we use a novel combination of Bachmair and Ganzingerâ??s model construction technique and a hierarchical construction of orderings and least fixpoints.

On the EA-style integrated processing of self-contained mathematical texts

A sound and complete first-order goal-oriented sequent-type calculus is developed with ``large-block'' inference rules. In particular, the calculus contains formal analogues of such natural proof-search techniques as handling definitions and applying auxiliary propositions.

Quantitative Information Flow, Relations and Polymorphic Types

This paper uses Shannon's information theory to give a quantitative definition of information flow in systems that transform inputs to outputs. For deterministic systems, the definition is shown to specialise to a simpler form when the information source and the known inputs jointly determine the inputs. For this special case, the definition is related to the classical security condition of non-interference and an equivalence is established between non-interference and independence of random variables. Quantitative information flow for deterministic systems is then presented in relational form. With this presentation, it is shown how relational parametricity can be used to derive upper and lower bounds on information flows through families of functions defined in the second order lambda calculus.

Precoder design for multi-antenna systems with temporally and spatially correlated fading channels

This paper addresses the problem of the design of a precoder for multiple transmit antenna communication systems with spatially and temporally correlated fading channels. Using the theories of matrix differential calculus, the paper derives a precoder for unitary space-time codes that can exploit the spatio-temporal correlation in the time-varying fading channels. The design criterion is based on minimizing the mean square error of the channel estimates. Computer simulation results show that a significant performance gain can be achieved by using the designed precoder.

Estimating intergenerational distribution preferences

Resource management decisions influence not only the output of the economy but also the distribution of utility between groups within the community. The theory of cost benefit analysis provides a means of incorporating distributional changes into the decision making calculus through the application of distributional or welfare weights. However, this practice has not been widely adopted in part due to difficulties in the estimation of distributional weights. This paper addresses this problem by using the stated preference method of choice modelling to estimate distributional weights suitable for inclusion in a cost benefit analysis framework. The findings of a choice modelling experiment designed to estimate community preferences with respect to intergenerational utility distribution illustrate the potential of this method in addressing distributional issues.

Measuring responses to dance : is there a 'grammer' of dance?

This paper reports a series of experiments that investigated how dance artists learn to see and understand dance. We measured, in real time, the responses of a number of dance artists and students, to a range of different dance stimuli to gain an understanding of how observers respond to structural elements of dance as they unfold over time.

A quantitative approach to analysing reliability of engagement responses to dance

Perhaps one of the most important end products of a dance work is how it  effects its observers (typically its audience, but also the dancers and choreographers). Of the many ways of discussing and analysing dance, one
approach in its infancy is quantification. Our research involves combining continuous response techniques and human response methods to see if we can tease out relationships between continuous, quantitative evaluative responses and the more qualitative choreographer intentions. The aim of this paper is to describe how evaluative responses can be quantified at all, then how they can be related to an unfolding dance work, and finally, how we can isolate ‘meaningful’ or ‘significant’ or ‘reliable’ evaluations of a dance work from those which are no more than a spurious set of not-very-useful numbers presented under the guise of a valid assessment.

Measuring audience response on-line : an evaluation of the portable audience response facility (pARF)

If it is the case that artists and art explore organization of the brain (Zeki & Lamb, 1994), then the investigation of response to artistic performance holds promise as a window to perceptual and cognitive processes. The portable Audience Response Facility (pARF) is an instrument for recording real‐time audience response (Stevens et al. 2009). Twenty, handheld, Personal Digital Assistants (PDAs) collect responses on customizable skin interfaces. The pARF server transmits the customizable options, synchronizes devices and collects data for export. In this paper we report ratings of the usability of the pARF that were collected after 37 participants had used it to continuously rate engagement along a single dimension while a female dance artist gave two performances of a short solo contemporary dance work. The motion of the dancer was also captured as she performed the piece but only usability rating data are reported here. Ratings indicate that the cognitive load imposed by continuously rating engagement while watching a dance performance was manageable and the pARF was easy to use. An extended familiarization phase may further reduce dual task demand.