Rechercher

[BCF16] Une preuve est (un programme) une histoire

Conférence Nationale avec comité de lecture : Actes des Vingt-septièmes Journées Francophones des Langages Applicatifs JFLA 2016, January 2016, pp.171-172, Saint Malo, France,

Mots clés: logique linéaire, narration interactive, atelier de preuve Coq.

Résumé: La narration computationnelle est un sous-domaine de l’Intelligence Artificielle, lié notamment aux problèmes de représentation des connaissances et en particulier la représentation des actions et du changement. On s'y intéresse aux objets narratifs (littéraires, interactifs, cinématographiques) pour les comprendre, les analyser, ou les construire, en proposant des techniques qui peuvent être mises en œuvre par des programmes et systèmes informatiques. C'est un domaine qui a des applications dans le domaine des jeux vidéos ou jeux utiles par exemple. Nous proposons de revenir dans cet exposé sur la motivation et les fondements d'un travail en cours, qui repose sur une connivence entre la structure des preuves en logique linéaire et la structure d'histoires interactives. Bien qu'ayant déjà donné lieu à une interprétation opérationnelle, cette approche a laissé des pistes inexplorées, surtout en ce qui concerne une normalisation et modularité de preuves/histoires dans un sous-ensemble ad hoc de la logique linéaire. Certaines idées ont été explorées en 2011 à l'aide de Coq et nous aimerions partager et échanger au sujet de nos projets actuels pour approfondir ce travail.

Collaboration: soc

BibTeX

@inproceedings {
BCF16,
title="{Une preuve est (un programme) une histoire}",
author=" A. Bosser and P. Courtieu and J. Forest and M. Aponte ",
booktitle="{Actes des Vingt-septièmes Journées Francophones des Langages Applicatifs JFLA 2016}",
year=2016,
month="January",
pages="171-172",
address="Saint Malo, France",
}