Franšais

A3PAT

ASSISTER  AUTOMATIQUEMENT LES ASSISTANTS DE
PREUVE AVEC DES TRACES

Take nothing on its looks; take everything on evidence. There's no better rule.
(Jaggers) C. Dickens Great Expectations.



Sceptical proof assistants like Coq or Isabelle enjoy a trustworthy verification kernel. For instance, Coq ensures soundness of a proof by typechecking a proof term.

However, those assistants lack automation.

Automation is hard to achieve in that context: in particular providing the results of external decision procedures is not sufficient. The proof assistant will refuse to handle a property if it does not come with a proof. That proof must be checked mechanically by the verification kernel. Hence, one has to give a certificate to the kernel.

This makes obvious the gap between proof assistants providing formal guaranties, and state-of-the-art automated tools the results of which have to be relied upon.

Objectives

The aim of Project A3PAT is to fulfil the important need for externalisation of proofs using rewriting techniques. We expect to achieve this aim in particular by defining generic ways of expressing certificates of reasonable size for possibly complex properties.

This amounts to:

Implementation

In the middle term, we wish to implement our solutions into a new version of the CiME rewriting tool which should be able to produce mechanically checkable traces, for instance by the Coq proof assistant.