|
 
|
[BCC11] Structural Analysis of Narratives with the Coq Proof Assistant
Rapport Scientifique : Date de dépot: 2011/03/01, Nb pages 16, (Tech. Rep.: CEDRIC-11-2061)Mots clés: Applications of Theorem Provers, Linear Logic, Formal Models of Narratives
Résumé:
This paper proposes a novel application of Interactive Proof Assistants for studying the formal properties of Narratives, building on recent work demonstrating the suitability of Intuitionistic Linear Logic as a conceptual model.
More specifically, we describe a method for modelling narrative resources and actions, together with constraints on the story endings in the form of an ILL sequent. We describe how well-formed narratives can be interpreted from cut-free proof trees of the sequent obtained using Coq. We finally describe how to reason about narratives at the structural level using Coq: by allowing to prove 2nd order properties on the set of all the proofs generated by a sequent, Coq assists the verification of structural narrative properties traversing all possible variants of a given plot.
Equipe:
sys
Collaboration:
soc
BibTeX
| @techreport { | |||
| BCC11, | |||
| title | = | "{Structural Analysis of Narratives with the Coq Proof Assistant}", | |
| author | = | "A. Bosser and M. Cavazza and P. Courtieu and J. Forest", | |
| number | = | "{CEDRIC-11-2061}", | |
| institution | = | "{CEDRIC laboratory, CNAM-Paris, France}", | |
| date | = | {01-03-2011}, | |
| pages | = | "16", | |
| } | |||
