[BCF11] Structural Analysis of Narratives with the Coq Proof Assistant.

Conférence Internationale avec comité de lecture : Interactive theorem proving (TPHOLs), August 2011, Vol. 6898, pp.55--70, Series Lecture Notes in Computer Science, Berg en Dal, The Netherlands,

Auteurs: A. Bosser , P. Courtieu , J. Forest , M. Cavazza

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 mod- elling 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 ob- tained using Coq. We finally describe how to reason about narratives at the structural level using Coq: by allowing one to prove 2nd order prop- erties 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

@inproceedings {
	BCF11,
	title	=	"{Structural Analysis of Narratives with the Coq Proof Assistant.}",
	author	=	" A. Bosser and P. Courtieu and J. Forest and M. Cavazza ",
	booktitle	=	"{Interactive theorem proving (TPHOLs)}",
	year	=	2011,
	month	=	"August",
	series	=	"Lecture Notes in Computer Science",
	volume	=	6898,
	pages	=	"55--70",
	address	=	"Berg en Dal, The Netherlands",
}