|
| EPSRC Reference: |
EP/F031114/1 |
| Title: |
Proof Theory and Constraint Satisfaction |
| Principal Investigator: |
Professor IP Gent |
| Other Investigators: |
|
| Researcher Co-investigator: |
|
| Project Partner: |
|
| Department: |
Computer Science |
| Organisation: |
University of St Andrews |
| Scheme: |
Standard Research |
| Starts: |
24 January 2008 |
Ends: |
23 August 2008 |
Value (£): |
44,237
|
| EPSRC Research Topic Classifications: |
| Fundamentals of Computing |
|
|
| EPSRC Industrial Sector Classifications: |
| No relevance to Underpinning Sectors |
|
|
| Related Grants: |
|
| Panel History: |
|
|
Summary |
Methods for "correct-by-construction" software development are finding more and more applications. A fundamental technology here is the application of methods based on the propositions-as-types/proofs-as-programs interpretation of constructive logics to particular
problems.
The research proposed here is twofold.
The first proposed research is the application of the proofs-as-programs methodology to a fundamental problem in constraint programming. We intend to constructively prove a theorem about establishing generalized arc consistency (GAC) whose proof will implicitly contain an algorithm for synthesizing watched literal propagators. This work will be collaborative between the visitor James Caldwell and Ian Gent and his colleagues working on the CIRCA project.
The second proposed research workpackage is more directly related to the proofs-as-programs methodology. In this part of the project, we propose to examine methods for
efficiently extracting programs from proofs in a certain class of logical system: multi-succedent intuitionistic sequent calculi. Theoretical results show that proofs in these calculi can be much smaller than proofs in the more widely used natural deduction based or single succedent based logical systems. Under the auspices of this grant we intend to explore methods of extracting programs from formal proofs in these more efficient proof systems. The goal here is to extract readable and efficient programs from these proofs. This research will be performed collaboratively between the visitor James Caldwell and Roy Dyckhoff.
|
| Final Report Summary |
This project brought James Caldwell from Wyoming to visit the University of St Andrews to work on two new collaborations with researchers at St Andrews. We have made significant progress in both areas and expect both collaborations to continue.
With Ian Gent and Peter Nightingale, Caldwell has worked on theoretical analysis of propagators in constraint programming. We have worked at a deeper level than we expected. We have generalised key notions from constraint programming, specifically the idea of "support". Doing this has slowed our short-term publication plans, but equally has led to more ambitious plans in the long term. The key notion we have developed is of "generalised support". Support is widely used in constraint programming, but with a rather narrow definition. Generalised support lets any form of evidence to be used to show that a constraint is in a consistent state. E.g., for the AllDifferent constraint, the evidence we require is a set of edges in a certain graph satisfying particular properties. By appropriate formal definitions, we have shown that complicated structures such as this can be used as support and propagated correctly.
Our first paper on this topic is "Generalized Support and Formal Development of Constraint Propagators". This is a theoretical paper showing key properties of generalised support, with proofs of correctness of some key propagators. To show the value of generalised support to the constraints community, we will next show that this improved understanding can improve the state of the art in constraint propagation. We will do this by showing that a uniform presentation of constraint propagators for generalised support can efficiently propagate practical constraints in Minion, our state of the art constraint solver.
The notion of generalised support was not in our original work plan at all, but arose naturally of asking the fundamental questions which were necessary to push through our theoretical approach to proving constraint propagators correct. This has led to what we expect to be an ongoing and fruitful collaboration with Caldwell. Nightingale plans to visit Caldwell in Wyoming during 2009.
With Roy Dyckhoff, Caldwell has explored the extraction of programs from formal proofs in a multi-succedent intuitionistic calculus m-G3i. Two extraction methods were explored: both used a tactic-based translation T to a single succedent calculus with Cut, followed by (a) cut-elimination and translation to natural deduction, or (b) translation to non-normal natural deductions and normalisation. These were implemented in OCaml, together with code for generating LaTeX for display of proofs. Satisfyingly readable normal ND terms were generated by both methods.
A comparison of this with a similar 1995 translation by Kreitz & Schmitt suggested that the key questions still to be resolved are:
(1) whether or not the two processes of (a) cut-elimination followed by translation to natural deduction and (b) translation to natural deduction and normalisation always yield the same outcomes given the same inputs. For at least one particular cut-elimination process, the answer appears to be positive.
(2) whether the mapping (from the space of derivations in m-G3i to the space of normal natural deductions) is surjective. We believe so, and have some confirmatory informal experimental results; a proper answer can only be given by a careful theoretical analysis. First, a concise notation for representing multi-succedent derivations is required.
Two papers are in preparation, on (a) the translation T and (b) the work mentioned in (1) above. The project's work was presented in July 2008 at the Workshop on Proof Theory in Bern. Dyckhoff and Caldwell intend to continue the theoretical investigations, as in (2) above; Caldwell intends to use the implemented system to synthesize programs from specifications expressed as types.
|
| Further Information: |
|
| Organisation Website: |
http://www.st-and.ac.uk |
|
|