POTTIER , Loïc

On étudie plusieurs voies pour formaliser les quotients dans le Calcul de Constructions Inductive: les quotients naïfs (en utilisant les travaux de [LW99] et [BB96],onmontre qu´ils conduisent à une incohérence), les quotients décidables, les quotients classiques de la théorie des types (comme ceux étudiés dans [Hof95], et finallement on propose...

La généralisation de termes est la notion duale de l'unification. Contrairement à l'unification, elle a été très peu étudiée, essentiellement par [Reynolds 70] et [Huet 76], et uniquement sur les termes sans théorie équationnelle. La généralisation de termes trouve des applications dans la compilation de systèmes de règles de réécriture, dans...

We study here \grobner\ bases of ideals which define toric varieties. We connect these ideals with the sub-lattices of $Z^d$, then deduce properties on their \grobner\ bases, and give applications of these results. The main contributions of the report are a bound on the degree of the \grobner\ bases, the fact that they contain Minkowski...

We propose a method to approximate the language of mathematicians by using amgiguities in the notations, in the context of type theory.

On présente ici une méthode permettant d'extraire de n'importe quel terme du CCI (toutes sortes confondues) un programme Ocaml acceptable par OCAML, et dont l'évaluation est efficace.

We caracterize a (affine) sub-group of Zn by a polynomial ideal and standard (Gröbner) basis. We show how to use these standard basis to solve directly many algorithmic problems on (affine) sub-groups and their non-negative parts : * the membership problem * the triviality problem * find the smallest non zero vector * find the minimal...

We describe how we connected three programs that compute Groebner bases to Coq, to do automated proofs on algebraic, geometrical and arithmetical expressions. The result is a set of Coq tactics and a certificate mechanism (downloadable at http://www-sop.inria.fr/marelle/Loic.Pottier/gb-keappa.tgz). The programs are: F4, GB \, and gbcoq. F4 and...

On donne de nouvelles bornes et de nouveaux algorithmes concernant les solutions minimales de systèmes diophantiens linéaires. Nos bornes sont simplement exponentielles en la dimension du système, alors que les bornes connues jusqu'il y a peu étaient doublement exponentielles.

International audience

This paper describes current results of Ofr (Optical Formula Recognition), a system for extracting and understanding mathematical expressions in documents. Such a tool could be really useful to be able to re-use knowledge in scientific books which are not available in electronic form. We currently also study use of this system for direct input...

This paper describes the design and the first steps of implementation of Ofr (Optical Formula Recognition), a system for extracting and understanding mathematical expressions in printed documents. Our approach clearly separate OCR step, geometrical treatments and syntactic analysis. In this paper we focus on the third part: we define a class of...

Integrating decision procedures in proof assistants in a safe way is a major challenge. In this paper, we describe how, starting from Hilbert's Nullstellensatz theorem, we combine a modified version of Buchberger's algorithm and some reflexive techniques to get an effective procedure that automatically produces formal proofs of theorems in...

On présente ici l'implémentation en OCaml d'une tactique Coq qui réalise une procédure d'élimination des quantificateurs pour les réels, basée sur la méthode de Hormander.