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.

Recycling workflows and services through discovery and reuse

Scientific workflows are becoming a valuable tool for scientists to capture and automate e-Science procedures. Their success brings the opportunity to publish, share, reuse and repurpose this explicitly captured knowledge. Within the myGrid project, we have identified key resources that can be shared including complete workflows, fragments of workflows and constituent services. We have examined the alternative ways these can be described by their authors (and subsequent users), and developed a unified descriptive model to support their later discovery. By basing this model on existing standards, we have been able to extend existing Web Service and Semantic Web Service infrastructure whilst still supporting the specific needs of the e-Scientist. myGrid components enable a workflow life-cycle that extends beyond execution, to include discovery of previous relevant designs, reuse of those designs, and subsequent publication. Experience with example groups of scientists indicates that this cycle is valuable. The growing number of workflows and services mean more work is needed to support the user in effective ranking of search results, and to support the repurposing process.