Proof certificates for some basic proof systems in classical logic
Encadrement :
Dale Miller, Parsifal team, INRIA-Saclay and LIX/Ecole Polytechnique
Description du sujet
Various computer systems produce proofs of logical statements and most of them are capable of outputting some evidence that they have successfully proved a theorem. Unfortunately, most of these artifacts that are produced are of limited use. For example, many interactive theorem provers use « proof scripts » as evidence that they have been steered to a complete proof. Such scripts can be replayed but they seldom have meaning to any other theorem prover and their replay value often does not survive a change in the prover’s version number.
In recent papers [Mil11a, Mil11b], Miller has proposed a proof theoretic framework for developing proof certificates that can be checked by simple proof checkers. This framework for proof certificates also provides flexibility in the proof styles that it can capture and in the trade-offs between the size of certificates and the computation costs of checking.
The goal of this internship is to develop this framework along the following lines.
- Classical (higher order) logic will be the main logic addressed.
- The proof systems to be captured by certificates are well know and popular and include resolution, Hilbert systems, tableaux, and natural deduction. See [NM09] and [SH09] where some details along these lines have been developed.
- A prototype certificate checker based on unification and bounded proof search will developed to check certificates representing proofs in all of these proof system. Such a prototype checker can be built using λProlog since it implements both (higher-order) unification and backtracking search.
This internship will take place within the funding context of the ProofCert project, a recently accepted ERC Advanced Investigator Award. This five year project (2012-2016) provides funding for PhD students covering a broad range to topics in a foundational approach to proof certificates.
Bibliography
The following bibliography is indicative of the kind of papers that will be part of this research effort.
- [LM09]
- Focusing and Polarization in Linear, Intuitionistic, and Classical Logic by Chuck Liang and Dale Miller. Theoretical Computer Science, 410(46), pp. 4747-4768 (2009) (doi, pdf). This paper is an extended version of a CSL07 paper.
- [M11a]
- Communicating and trusting proofs: The case for broad spectrum proof certificates by Dale Miller. Draft dated 7 Septemer 2011. (pdf).
- [M11b]
- A proposal for broad spectrum proof certificates by Dale Miller. Accepted to CPP 2011: First International Conference on Certified Proofs and Programs, 7-9 December 2011, Taiwan. Draft dated 30 October 2011: (pdf). Slides: pdf. See also the description of the panel on Communicating and trusting proofs held during this meeting.
- [NM09]
- A framework for proof systems by Vivek Nigam and Dale Miller. Journal of Automated Reasoning, 2010, pp. 157-188. (pdf)
- [SH09]
- Using LJF as a Framework for Proof Systems by Anders Starcke Henriksen. Technical Report, University of Copenhagen, 2009. [http]
