MRG home page · Research · Publications · Projects · Software · People

Deductive Synthesis of of Plans with Linear Logic
(with applications to Grid Workflows for e-Science)


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.


Related Projects

Other Links:

Mathematical Reasoning Group, Informatics Forum, 10 Crichton Street, Edinburgh, EH8 9AB, Scotland
Tel: +44 (0)131 650 2733      Fax: +44 (0)131 650 6899
Please send corrections and suggestions for this page to the Lucas Dixon
Unless explicitly stated otherwise all material on this web site is copyright © The University of Edinburgh.