|
 
|
[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", | |
| } | |||
