dr. Sorin STRATULAT
Associate Professor in Computer Science
University Paul Verlaine
Metz
Franta
-----------------------------------
          
Automatic "Descente Infinie" Induction Reasoning
-----------------------------------
          
ABSTRACT
-----------------------------------
We present a framework and a methodology to build and analyse
provers using the "Descente Infinie" induction principle. Different
proof techniques, like those based on implicit induction and
saturation, are uniformly presented as applications of this
principle. The framework offers a clear separation between logic
and computation, by the means of 

1)an abstract inference system that defines the maximal sets
of induction hypotheses available at every step of a proof,
and 

2)reasoning modules that perform the computation and allow
for modular design of the concrete inference rules.

The methodology is applied to build a simple concrete implicit
induction prover and to improve an existing implicit induction
prover in order to deal with industrial-size case studies.
          
SHORT CV
-----------------------------------
Absolvent al Universitatii "POLITEHNICA" din Bucuresti, Sorin
Stratulat a urmat studiile cu un master si un doctorat in informatica
ale Universitatii "Henri Poincare" din Nancy, Franta. 
Incepand cu 2001, a facut mai multe stagii postdoctorale la
SRI (Stanford Research Institute) International din California,
Statele Unite, DIST din Genova, Italia, INRIA din Sophia Antipolis,
Franta.
In momentul de fata, este "Maitre des Conferences" la Universitatea
"Paul Verlaine" din Metz, Franta.
Principalul domeniu de interes in activitatea sa de cercetare
este
demonstrarea automata. 
Este autorul unui cadru teoretic de dezvoltare al demonstratoarelor
bazate pe inductie, cu aplicatii practice in domeniul telecomunicatiilor
si al "cardurilor inteligente" (smartcards).