Overview
The aim of the project is to evaluate the applicability of deductive
synthesis to the problems of rapid customised assembly and automated
recovery failure of Grid applications. A formal language will be
developed in which both the implementation and the specification of
Grid applications can be represented. A proof-plan based deductive
synthesis system will be developed for this language and tested on the
semi-automatic (re-) assembly various Grid applications from their
specifications. If time allows, the application of analogical theorem
proving to the reassembly of Grid applications will also be tested.
Grant Information
"Application of Deductive Synthesis Techniques to the Rapid Assembly
and Re-Assembly of Grid Applications". EPSRC grant GR/S25388 (RR36961)
(funded by e-Science Core Programme). Grant Duration: 1 Jan 2003 -- 31
Dec 2005. It was originally a PhD Project undertaken by Bin Yang. PhD
Start Date: 1 Oct 2002. The grant holders are Alan Bundy and Alan
Smaill. From the 1st of September to the 30th Feb, work is being done
by Lucas Dixon.
Current Directions
We intend to formalise intuitionistic linear logic in Isabelle/HOL
with proof terms. We will then and develop tools to
support the synthesis of
proof terms that can be interpreted as plans. We intend to examine
applications in the composition of proof tools as used by Zimmer, Meier, Sutcliffe
and Zhang in Integrated
Proof Transformation Services as well as to Astrophysics service
composition.
Publications
- Planning as Deductive
Synthesis in Intuitionistic Linear Logic. L. Dixon, A. Smaill, A. Bundy. Informatics Technical Report 0786, [15 pages, 2006]
- Deductive Synthesis of Workflows for E-Science (ps.gz) by B. Yang, A. Bundy,
A. Smaill, L. Dixon, in the SIGAW Workshop of CCGrid 2005,
Cardiff.
- Inferring Quality of Service Properties for Grid Applications (PDF) by Lin Yang, CS poster,
Presented in EPSRC e-Science Meeting 2004, 26th March, NeSC,
Edinburgh, UK.
- Formalising the Grid - the 1st Step to Automate Grid
Application Assembly using Deductive Synthesis (PDF) by Bundy, Smaill, Yang,
in Proceedings of UK e-Science Second All Hands Meeting 2003, page
337, 2-4th September, Nottingham, UK. Cox, S., Eds.
Related Projects
- Inferring Quality of Service Properties
for Grid Applications. The project is evaluating the applicability
of compositional calculi for estimating quality of service (QoS)
properties arising in the development of an e-Science infrastructure
such as the Grid.
- Ozan
Kahramanogullari is using an extension of linear logic, which has
evolved into the Calculus of
Structures, and also developing proof search techniques for his
system. In his own words, he is "... developing a common language for
concurrency and planning that aims at bringing these two fields
closer. Such a language will allow to transfer mathematical notions
from concurrency to planning, and provide a platform for a structural
analysis of plans.". This work is in the Maude system. Papers are
available at http://alessio.guglielmi.name/res/cos/index.html.
- The PhD thesis of Jinghai Rao, Semantic Web
Service Composition via Logic-based Program Synthesis, describes
using linear logic for the composition of web services. This work uses
a loose coupling of systems which are combined using an agent
framework and translations between the various languages. For linear
logic proof construction, they use LL-prover. They
argue that linear logic based composition of web services is feasible,
and that they have provided a flexible and scalable agent based
system. However, they do not describe any large case studies. It may
be that case studies are described in the associated papers.
- Paulo Pinheiro da Silva, Deborah L. McGuinness and Richard
Fikes. A Proof Markup Language for Semantic Web Services. Information
Systems. [Accepted for publication.] and Paulo Pinheiro da Silva,
Patrick Hayes, Deborah L. McGuinness, Richard Fikes and Priyendra
Deshwal. Towards Checking Hybrid Proofs. Technical Report KSL-05-01,
Knowledge Systems Laboratory, Stanford University, USA, 2005. see: http://iw.stanford.edu/documents_papers.html
Other Links:
