Foreword
The procedural reconstruction is a feature of the proof assistant Matita for translating the
system's logical representation of formalized mathematical knowledge
(mainly of formalized proofs) into the
system's high-level specification language.
This feature has its justification in the actual fact that proof
assistants allow to edit some knowledge only starting from its
high-level representation, so the adaptation and maintenance of this
knowledge can not be performed at the logical level.
The knowledge to which this translation applies, can come from any
source that contributes to HELM
(that is the digital library of Matita).
For instance it can come from another digital library or from another
proof assistant. Therefore this transformation may help the
cross-platform maintenance of the certified specifications (as in the
case of the formal
system λδ).
This transformation is focused on proofs. In general terms a proof has
two main aspects:
- the declarative
aspect is concerned with the contents
of the proof, that is what is
proved step by step;
- the procedural
aspect is concerned with the structure
of the proof, that is how
the proof is carried out step by step.
Evidently a procedural representation of a
proof is less readable for the human user, but
appears easier to maintain.
In fact adapting or maintaining a
proof usually means changing some aspects of its contents while
trying to preserve its structure.
Since a proof may need some transformation before being translated, for
the user convenience we preprocess the proof with an optimizing procedure. An optimized proof does not contain
detours or unused information and is normalized according to the direct proof paradigm to possibly
enhance its readability and ease its maintenance.
News 
- February 2009. The
first journal paper on the procedural reconstruction is accepted for
publication.
- November 2008. This
Web site is online.
- July 2008. The
certified specification of the formal system λδ
(coming from Coq 7.3.1) is fully
reconstructed (762 proofs).
- December 2006. The
implementation of procedural reconstruction begins.
Documentation 
- F. Guidi: Procedural
Representation of CIC proof Terms (2009-02). Accepted
for JAR special issue on PLMMS.
- F. Guidi: Procedural
Representation of CIC Proof Terms (2007-06). In local proc. of PLMMS
2007. RISC-LINZ
Report Series 07-10 (3120), University of Linz, pp. 36-52.
- F. Guidi: Procedural
Representation of CIC Proof Terms (2009-03). Communication at the
University of Bologna (slides).
- F. Guidi: Procedural
Representation of CIC Proof Terms (2007-06). Communication at PLMMS
2007 (slides).
Implementation 
The procedural reconstruction is activated by invoking the Matita
high-level command inline.
The parameters of the inline
command affecting the procedural reconstruction procedure, are the
following:
- Procedural. This
parameter is mandatory to activate the procedural reconstruction
procedure.
- level=n. This
optional parameter selects the procedural reconstruction level (i.e. the set of tactics
exploited by the reconstruction procedure). If omitted, the level
defaults to the highest value. The currently implemended levels are:
- nodefaults. This
parameter inhibits the use of the
tactics (i.e. rewrite)
depending on the Matita high-level command default.
- depth=n.
Undocumended yet.
|
