Proof Theory and Constraint Satisfaction

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 particularproblems. 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 forefficiently 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.