Ceptre can be viewed as an explication of a new methodology for understanding games based on linear logic, a formal...

Ceptre can be viewed as an explication of a new methodology for understanding games based on linear logic, a formal logic concerned with resource usage. We present a correspondence between gameplay and proof search in linear logic, building on prior work on generating narratives. In Ceptre, we introduce the ability to add interactivity selectively into a generative model, enabling inspection of intermediate states for debugging and exploration as well as a means of play.
http://lambda-the-ultimate.org/node/5216