| EPSRC Reference: |
GR/J46616/01 |
| Title: |
SEARCH MODULES I: REPRESENTATION AND COMBINATION OF PROOF PROCEDURES |
| Principal Investigator: |
Wallen, Professor L |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Computer Science |
| Organisation: |
University of Oxford |
| Scheme: |
Standard Research (Pre-FEC) |
| Starts: |
01 January 1994 |
Ends: |
31 December 1996 |
Value (£): |
137,894
|
| EPSRC Research Topic Classifications: |
|
| EPSRC Industrial Sector Classifications: |
|
| Related Grants: |
|
| Panel History: |
|
|
Summary on Grant Application Form |
|
To develop a theory of representation of object level proof procedures within the setting of a logical framework To develop an experimental computer system for designing and combining proof procedures for objective languages. To test the theory and implementation on important examples involving hybrid reasoning.Progress:The project has progressed along three main lines:1. Proof-search via the LF logical frameworkA formal theory for type similarity in the LF has been designed which is Church-Rosser and strongly normalising [BR94]. A representation of lII- unification as an inference system has been developed, which uses type similarity and through which unification for encoded logics is induced [BW95]. A matrix characterisation of proof-search in the RII-calculus is under investigation. A Kripke-style model theory for the LF (addressing both l-calculus and framework issues ) has been developed using fibred category theory [P9Sa]. Kripke-logical relations for this system are under investigation. A research monograph (CUP) is in preparation [P96 (expected)]. 2. Syntax and Semantics of Proof-searchA calculus for partial classical sequent proofs based on linear logic has been defined [RPW94]. this is being simplified using Parigot's l--calcululs. Modelling partial proofs as objects in a suitable domain is being explored and notions of search (for an 'answer' to a 'question') have been developed from simple model-theoretic assumptions about constructions [Ri94]. Optimisation of proof search by relaxing restrictions on the order of search steps is under investigation ink this semantic framework. 3. Process-theoretic Models of Proof-searchProof-search has been viewed as a planning problem via an algebraic theory of processes. Preliminary indications are that proof-search problems can be fruitfully formulated in these terms. This is a surprising and exciting development [PPrM95, PrPM95, MPrP95]. B=J.Brown, P=D.Pym, R=E.Ritter, Ri=A Richardson, W=L.Wallen, M=D.Murphy (Birmingham), Pr=L.Pryor (Edinburgh). Preprints of all publications are available from the P.I.s
|
|
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.ox.ac.uk |