Output details
11 - Computer Science and Informatics
Teesside University
Structural analysis of narratives with the Coq proof assistant
<11> This paper presents a first operationalisation of the work presented in our ECAI 2010 paper. We use the Coq proof assistant to provide a novel way to analyse and evaluate computational narratives through an original method for evidencing common properties of narratives generated by a set of initial conditions. We also establish correspondences between computational narrative problems and proof representation and modularity problems. Narrative modelling provides a domain-specific and restricted context where these problems may be addressed in the future. ITP, formerly TPHOL, is now a part of FLOPS. It is the main conference for the interactive theorem proving community.