Details of Grant 

EPSRC Reference:	GR/J14745/01
Title:	ALGORITHMIC DEDUCTION BASED ON LABELLED TABLEAUX
Principal Investigator:	Broda, Dr K
Other Investigators:	Gabbay, Professor D Cunningham, Mr R
Researcher Co-Investigators:
Project Partners:
Department:	Computing
Organisation:	Imperial College London
Scheme:	Standard Research (Pre-FEC)
Starts:	01 October 1993	Ends:	30 April 1996	Value (£):	172,909
EPSRC Research Topic Classifications:	Fundamentals of Computing
EPSRC Industrial Sector Classifications:
Related Grants:
Panel History:
Summary on Grant Application Form
To develop a uniform theory of algorithmic analytic deduction for the application of logic to computational problems: by shifting from formulas to labelled formulas in the spirit of Gabbays unifying approach of Labelled Deductive Systems; developing a uniform theory of the generalised notion of analytic tableaux with labels; incorporating forms of unification into the method;introducing refinements to systematise and reduce the search space, for example the KE refinement; in particular, to develop our approach for resource logics.Progress:i) The KE-tableau method for the multiplicative fragment of sub-structural logics has been implemented, together with a separate, and new, associative commutative with identity unification algorithm, used for a Linear Logic theorem prover. (See (3).) The resulting prover is flexible enough to be used to give a form of abduction of resources, that accounts for every resource used in a proof. This is in contrast with more usual sequent based approaches. (To be reported in (6).)ii) An extension of the unification algorithm to include the *operator, introduced through negation (see (1) is currently being investigated.iii) The relationship between KE tableaux and Natural Deduction has been investigated and reported in (4). In addition, some well-known properties of Horn clauses have been reproven within a proof theoretic framework and will be reported in (7).iv) The basic LDS method for sub-structural logics extends to logics other than Linear Logic (see (1) and a constraint based unification algorithm is being developed with a 4th year MEng student for Intuitionistic Logic.v) The incorporation of the additative connectives of sub-structural logics within the LDS framework is also in preparation, so that a full Linear Logic theorem prover can be implemented.(1) A Generalisation of Analytic Deduction via Labelled Deductive Systems. Part I: Basic Substructural Logics. M. DAgostino and D. Gabbay, Journal of Automated Reasoning 13 (2) (1994), pp 243-281. 2) The Taming of the Cut. M. DAgostino and M. Mondadori, Journal of Logic and Computation 4 (1994), pp 285-319.(3) KE-Tableaux for a Fragemnt of Linear Logic. K. Broda and M. Finger, Extended Abstract to be presented at the Workshop on Theorem Proving with Analytic Tableanux and Related Methods, Koblenz, Germany, 1995.(4) Finding Proofs in Substructural Logics. K. Broda and M. DAgostino, presented at the Workshop in Proof Theory and Linear Logic and Categorical Grammars, Rome, Italy, 1994.(5) Poppers Logical System and the Teaching of Logic. M. DAgostino, M. Mondadori. and K. Broda, Proc. of the Conf. of Epistemology of Karl Popper, Csena, Italy, 1994.(6) Proof Search and Resource Abduction in Linear Logic. K. Broda, M. DAgostino, M. Finger and D. Gabbay.(7) Analytic Deduction, Horn Clauses and Cut Elimination. K. Broda and M. DAgostino.
Key Findings
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Potential use in non-academic contexts
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Impacts
Description This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk Summary Date Materialised
Sectors submitted by the Researcher
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Project URL:
Further Information:
Organisation Website:	http://www.imperial.ac.uk