Ph.D. Thesis Chris Martens

Abstract

Interactive storytelling weaves together deep computational ideas with humanity's rich history of story and play, providing an important context for tools and languages to be built. At the same time, formal specification languages offer a palette of representation and inference techniques typically reserved for the analysis of programming languages and complex deductive systems. This thesis connects problems in the interactive storytelling domain to solutions in formal specification.

Specifically, we examine narrative from a structural point of view and observe that alternative narrative paths play a complementary role to simultaneous interacting timelines. Linear logic provides the representational tools necessary to investigate this structure, and by extending the correspondence to proofs and proof construction, we find a suite of computational possibilities. We present three efforts toward realizing those possibilities: (1) the use of linear logic programming to generate narratives; (2) a new programming language for authoring interactive narratives, games, and simulations; and (3) techniques for stating and proving design-level program properties.

We find that linear logic programming, enriched with a minimal extension to its logical semantics, enables a wide range of programming idioms and domain encodings. As evidence, we give five case studies, including social simulation, combat-based adventure games, and board games. To support reasoning about design correctness, we present techniques for stating and proving program invariants, as well as a decidability proof for automatically checking those invariants for a large fragment of the language.

These findings show that linear logic is a fruitful representation language to serve as the basis for modeling and executing interactive worlds, and they invite future investigations on using proof-theoretic methodologies for creative systems.

Submitted Document

Here is the complete 229-page PDF document that was submitted to the printers.

The thesis, by chapter

• Chapter 1: Introduction
• Chapter 2: Linear Logic for Narrative Structure
• Chapter 3: Linear Logic Programming for Narrative Generation
• Chapter 4: Ceptre: A Linear Logic Language for Interactive Programs
• Chapter 5: Case Studies
• Chapter 6: Reasoning About Linear Logic Programs
• Chapter 7: Conclusion

All the other bits:

• Frontmatter, including acknowledgments
• Appendices, including typing rules and code listings
• Bibliography
• Source files for the submitted version (.tex, .bib, .cls, and .sty)
• Slides from the defense talk

Progress graph