Le dernier séminaire a eu lieu le 25 Octobre 2024

Les 3 derniers séminaires du LIM

Méthodologie de classification par approche descriptive hybride numérique/symbolique

Animé par Cyprien Pankowski, le 25 Octobre 2024 à 14:00:00

La méthodologie de classification par approche descriptive consiste à caractériser les données en s'appuyant sur des descripteurs extraits de celles-ci. Dans le cadre de la reconnaissance vocale des cétacés, cette approche implique d'abord une analyse détaillée des vocalises enregistrées, en identifiant des paramètres acoustiques tels que la fréquence, la durée, et les motifs temporels. Ensuite, ces descripteurs permettent de regrouper et de classifier les vocalises en fonction de leurs similarités. La description symbolique, telle que l'espèce, le lieu d'enregistrement, l'auteur de l'enregistrement, sont aussi des informations permettant la classification.

à préciser

Animé par Frédérick Fabre Ferber, le 25 Octobre 2024 à 15:15:00

Automated Theorem Proving for Prolog Verification

Animé par Fred Mesnard, le 24 Octobre 2024 à 16:30:00

LPTP (Logic Program Theorem Prover) est un démonstrateur de théorèmes interactif basé sur la déduction naturelle pour des programmes Prolog purs avec la négation par échec, l'unification avec test d'occurrence, et un ensemble restreint mais extensible de prédicats prédéfinis. Avec LPTP, conçu au milieu des années 90 par Robert F. Stärk, il est possible de prouver formellement la terminaison et la correction partielle de tels programmes Prolog. D'un point de vue théorique, dans ses publications sur LPTP, Stärk associe un ensemble d'axiomes du premier ordre IND(P) au programme Prolog P considéré. IND(P) contient la théorie de l'égalité de Clark pour P, les définitions de succès, d'échec et de terminaison pour chaque procédure logique définie par l'utilisateur dans P, des axiomes reliant ces trois points de vue, et un schéma d'axiome pour prouver des propriétés inductives. En pratique, LPTP est utilisé comme un éditeur de preuves dédié où ces axiomes sont intégrés. Nous proposons d'expliciter ces axiomes sous forme de formules du premier ordre (FOF), et d'appliquer des démonstrateurs de théorèmes automatisés pour vérifier la propriété d'intérêt. Nous évaluons cette approche sur un ensemble d'environ 400 propriétés de programmes Prolog tirées de la bibliothèque disponible avec LPTP.