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:

- 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
C*i*ME
rewriting tool which should be able to produce *mechanically
checkable traces*, for instance by the Coq proof assistant.