Français

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.

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:

• defining a language for traces, expressive enough w.r.t the diversity of problems tackled, and allowing traces of reasonable size;
• formalising and providing models for various notions involved such as critical pairs, unification, termination...
  A significant library developed in this framework is available.

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.

• Members
• Tools and Publications