Skip to Main content Skip to Navigation
New interface

Internship report MPRI 2 Reverse engineering on arithmetic proofs

2 DEDUCTEAM - Deduction modulo, interopérabilité et démonstration automatique
LSV - Laboratoire Spécification et Vérification [Cachan], Inria Saclay - Ile de France
Abstract : dedukti is a logical framework that implements the λΠ− modulo theory, an extension of the simply typed lambda calculus with dependent types and rewriting rules. It aims to be a back-end for other proof checkers by compiling proofs from these proof checkers to dedukti. This may also increase re-usability of proofs between proof checkers. However if a logic is more powerful than an other, a theorem in the first logic may not be a theorem in the second. During this internship, we consider arithmetic theorems since many proof checker are able to check arithmetic proofs. One problem that we study in this master thesis is to translate arithmetic proofs coming from a powerful proof checker, -- in our case matita -- to a less powerful proof checker -- HOL-- . This translation needs to modify the logic used in proofs and that is why dedukti is handy here. But a lot of arithmetic theorems are proved also by automatic provers. Indeed, today a lot of easy arithmetic theorems are proved by this kind of tool. But most of them do not give a proof if it claims to prove a theorem. Since for these kind of tool, constructing a full proof may be tiresome, they prefer to give a certificate , a sketch of a proof. However, any automatic prover can implement its own certificate format. To answer this problem, Zakaria Chihani & Dale Miller proposed a certificate framework: Foundational Proof Certificate (FPC) [CMR13]. This framework aims to provide a certificate format shared by many automatic provers so that from the latter, a full proof might be reconstructed. However, for now, no certificate format is given for arithmetic proofs. A second problem addressed in this internship is to answer what kind of certificate is needed for arithmetic proofs (arithmetic without multiplication).
Document type :
Master thesis
Domain :
Complete list of metadata

https://hal.inria.fr/hal-01424816
Contributor : François Thiré Connect in order to contact the contributor
Submitted on : Monday, January 2, 2017 - 10:35:38 PM
Last modification on : Friday, February 4, 2022 - 3:12:13 AM

Licence

Distributed under a Creative Commons Public Domain Mark 4.0 International License

Identifiers

• HAL Id : hal-01424816, version 1

Citation

François Thiré. Internship report MPRI 2 Reverse engineering on arithmetic proofs. Computer Science [cs]. 2016. ⟨hal-01424816⟩

Record views

Files downloads