Méthodes de formalisation des connaissances et des raisonnements mathématiques : aspects appliqués et théoriques
Institution:
Paris 12Disciplines:
Directors:
Abstract EN:
We study the means of presentation of mathematical knowledge and reasoning schemes. Our research aims at an automated system for verification of formalized mathematical texts. In this system, a text to verify is written in a formal language which is close to the natural language and style of mathematical publications. Our intention is to exploit the hint which are given to us by the "human" form of the problem : definitions, proof scemes, nouns denoting classes of objects, etc. We describe such a language, called ForTheL. Verification consists in showing that the text is "sensible" and "grounded", that functions and relations are applied within the domain, according to the definitions, and assertions follow from their respective premises. A formal definition of a correct text relies on a sound sequent calculus and on the notion of local validity (local with respect to some occurrence inside a formula). Proof search is carried out on two levels. The lower level is an automated theorem prover based on a combinatorial procedure. We introduce a variant of connection tableaux which is sound and complete in the first-order logic with equality. The higher level is a "reasoner" which employs natural proving techniques in order to filter, simplify, decompose a proof task before passing it to the prover. The algorithms of the rasoner are based on transformations that preserve the locally valid propositions. The proposed methods are implemented in the proof assistant SAD.
Abstract FR:
Nous étudions les moyens de présentation des connaissances et des schémas du raisonnement mathématiques. Notre recherche est destinée à un système de vérification de textes mathématiques formalisés. Dans ce système, la texte à vérifier est écrit dans un langage formel proche de la langue naturelle et le style des publications mathématiques. Notre intention est d'exploiter les indices que la forme "humaine" du problème nous donne : les définitions, les schémas de preuve, les substantifs qui désignent des classes d'objets. Un tel langage, appelé ForTheL, est décrit. La vérification consiste en la démonstration que le texte est "sens" et "fondé", c'est-à-dire que les fonctions et les relations sont employées dans leurs domaines, conformément aux définitions, et les assertions se déduisent des prémisses. La définition formelle d'un texte correct repose sur un calcul séquentiel cohérent ainsi que sur la notion de validité locale (par rapport à une occurrence à l'intérieur d'un formule). La recherche de preuve est effectuée à deux niveaux. Le niveau bas est un démonstrateur automatique basé sur une procédure combinatoire. Nous introduisons une variante des tableaux de connexions cohérente et complète en logique du premier ordre avec égalité. Le niveau haut est un "raisonneur" qui emploie des techniques naturelles de démonstration pour filtrer, simplifier, décomposer une tâche de preuve avant de la passer au démonstrateur. Les algorithmes du raisonneur se basent sur les transformations qui préservent les propositions localement valides. Les méthodes proposées sont implantées dans l'assistant de preuve SAD.