{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T10:52:59Z","timestamp":1742986379337,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642228629"},{"type":"electronic","value":"9783642228636"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-22863-6_7","type":"book-chapter","created":{"date-parts":[[2011,8,8]],"date-time":"2011-08-08T09:47:55Z","timestamp":1312796875000},"page":"55-70","source":"Crossref","is-referenced-by-count":2,"title":["Structural Analysis of Narratives with the Coq Proof Assistant"],"prefix":"10.1007","author":[{"given":"Anne-Gwenn","family":"Bosser","sequence":"first","affiliation":[]},{"given":"Pierre","family":"Courtieu","sequence":"additional","affiliation":[]},{"given":"Julien","family":"Forest","sequence":"additional","affiliation":[]},{"given":"Marc","family":"Cavazza","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"7_CR1","series-title":".","volume-title":"ECAI 2010 Frontiers in Artificial Intelligence and Applications","author":"A.G. Bosser","year":"2010","unstructured":"Bosser, A.G., Cavazza, M., Champagnat, R.: Linear logic for non-linear storytelling. In: ECAI 2010 Frontiers in Artificial Intelligence and Applications, vol.\u00a0215. IOS Press, Amsterdam (2010)"},{"key":"7_CR2","unstructured":"Br\u00e9mond, C.: Logique du R\u00e9cit. Seuil (1973)"},{"key":"7_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/11944577_7","volume-title":"Technologies for Interactive Digital Storytelling and Entertainment","author":"M. Cavazza","year":"2006","unstructured":"Cavazza, M., Pizzi, D.: Narratology for interactive storytelling: A critical introduction. In: G\u00f6bel, S., Malkewitz, R., Iurgel, I. (eds.) TIDSE 2006. LNCS, vol.\u00a04326, pp. 72\u201383. Springer, Heidelberg (2006)"},{"key":"7_CR4","volume-title":"ACM SIGCHI Advances in Computer Entertainment Technology (ACE)","author":"F. Coll\u00e9","year":"2005","unstructured":"Coll\u00e9, F., Champagnat, R., Prigent, A.: Scenario analysis based on linear logic. In: ACM SIGCHI Advances in Computer Entertainment Technology (ACE). ACM Press, New York (2005)"},{"key":"7_CR5","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1145\/1706356.1706370","volume-title":"ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM 2010)","author":"\u00c9. Contejean","year":"2010","unstructured":"Contejean, \u00c9., Courtieu, P., Forest, J., Paskevich, A., Pons, O., Urbain, X.: A3PAT, an Approach for Certified Automated Termination Proofs. In: ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM 2010), pp. 63\u201372. ACM, New York (2010)"},{"key":"7_CR6","unstructured":"Contejean, E., Courtieu, P., Forest, J., Pons, O., Urbain, X.: The CiME Rewriting Toolbox, Version 3, http:\/\/cime.lri.fr"},{"key":"7_CR7","unstructured":"Dalrymple, M., Lamping, J., Pereira, F.: Linear logic for meaning assembly. In: Proceedings of the Workshop on Computational Logic for Natural Language Processing (1995)"},{"key":"7_CR8","unstructured":"Dixon, L., Smaill, A., Bundy, A.: Verified planning by deductive synthesis in intuitionistic linear logic. In: ICAPS Workshop on Verification and Validation of Planning and Scheduling Systems (2009)"},{"issue":"2","key":"7_CR9","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/s10849-008-9079-0","volume":"18","author":"L. Dixon","year":"2009","unstructured":"Dixon, L., Smaill, A., Tsang, T.: Plans, actions and dialogues using linear logic. Journal of Logic, Language and Information\u00a018(2), 251\u2013289 (2009)","journal-title":"Journal of Logic, Language and Information"},{"issue":"1","key":"7_CR10","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","volume":"50","author":"J.Y. Girard","year":"1987","unstructured":"Girard, J.Y.: Linear logic. Theoretical Computer Science\u00a050(1), 1\u2013102 (1987)","journal-title":"Theoretical Computer Science"},{"key":"7_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"52","DOI":"10.1007\/BFb0014972","volume-title":"TAPSOFT \u201987 Proceedings of the International Joint Conference on Theory and Practice of Software Development, Pisa, Italy, March 23 - 27 1987.","author":"J.Y. Girard","year":"1987","unstructured":"Girard, J.Y., Lafont, Y.: Linear logic and lazy computation. In: Ehrig, H., Levi, G., Montanari, U. (eds.) TAPSOFT 1987. LNCS, vol.\u00a0250, pp. 52\u201366. Springer, Heidelberg (1987)"},{"key":"7_CR12","unstructured":"Grasbon, D., Braun, N.: A morphological approach to interactive storytelling. In: Proceedings of the Conference on Artistic, Cultural and Scientific Aspects of Experimental Media Spaces (cast01) (2001)"},{"key":"7_CR13","unstructured":"Greimas, A.J.: S\u00e9mantique structurale: recherche et m\u00e9thode. Larousse (1966)"},{"key":"7_CR14","doi-asserted-by":"crossref","unstructured":"Gupta, V., Lamping, J.: Efficient linear logic meaning assembly. In: Proceedings of the 17th International Conference on Computational Linguistics (1998)","DOI":"10.3115\/980451.980924"},{"key":"7_CR15","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1016\/S0743-1066(96)00138-0","volume":"31","author":"A. Kakas","year":"1997","unstructured":"Kakas, A., Miller, R.: A simple declarative language for describing narratives with actions. Journal of Logic Programming\u00a031, 157\u2013200 (1997)","journal-title":"Journal of Logic Programming"},{"key":"7_CR16","unstructured":"Kalvala, S., Paiva, V.D.: Mechanizing linear logic in isabelle. In: 10th International Congress of Logic, Philosophy and Methodology of Science (1995)"},{"key":"7_CR17","volume-title":"Narrative Intelligence: Papers from the AAAI Fall Symposium","author":"R.R. Lang","year":"1999","unstructured":"Lang, R.R.: A declarative model for simple narratives. In: Narrative Intelligence: Papers from the AAAI Fall Symposium. AAAI Press, Menlo Park (1999)"},{"key":"7_CR18","first-page":"109","volume-title":"Advances in Linear Logic","author":"P. Lincoln","year":"1994","unstructured":"Lincoln, P.: Deciding provability of linear logic formulas. In: Advances in Linear Logic, pp. 109\u2013122. Cambridge University Press, Cambridge (1994)"},{"issue":"2","key":"7_CR19","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1016\/0304-3975(93)90008-H","volume":"113","author":"M. Masseron","year":"1993","unstructured":"Masseron, M.: Generating plans in linear logic: I i. a geometry of conjunctive actions. Theoretical Computer Science\u00a0113(2), 371\u2013375 (1993)","journal-title":"a geometry of conjunctive actions. Theoretical Computer Science"},{"issue":"2","key":"7_CR20","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1016\/0304-3975(93)90007-G","volume":"113","author":"M. Masseron","year":"1993","unstructured":"Masseron, M., Tollu, C., Vauzeilles, J.: Generating plans in linear logic: I. actions as proofs. Theoretical Computer Science\u00a0113(2), 349\u2013370 (1993)","journal-title":"Theoretical Computer Science"},{"key":"7_CR21","doi-asserted-by":"publisher","first-page":"513","DOI":"10.1093\/logcom\/4.5.513","volume":"4","author":"R. Miller","year":"1994","unstructured":"Miller, R., Shanahan, M.: Narratives in the situation calculus. Journal of Logic and Computation\u00a04, 513\u2013530 (1994)","journal-title":"Journal of Logic and Computation"},{"key":"7_CR22","series-title":"Lecture Notes in Computer Science","volume-title":"Theorem Proving in Higher Order Logics","author":"J. Power","year":"1999","unstructured":"Power, J., Webster, C.: Working with linear logic in coq. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Th\u00e9ry, L. (eds.) TPHOLs 1999. LNCS, vol.\u00a01690. Springer, Heidelberg (1999)"},{"key":"7_CR23","doi-asserted-by":"crossref","unstructured":"Propp, V.: Morphology of the Folktale. University of Texas Press (1968)","DOI":"10.7560\/783911"},{"key":"7_CR24","volume-title":"KR","author":"R. Reiter","year":"2000","unstructured":"Reiter, R.: Narratives as programs. In: KR. Morgan Kaufmann, San Francisco (2000)"},{"key":"7_CR25","series-title":"Lecture Notes in Computer Science","first-page":"75","volume-title":"Theorem Proving in Higher Order Logics","author":"M. Sadrzadeh","year":"2003","unstructured":"Sadrzadeh, M.: Modal linear logic in higher order logic: An experiment with coq. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol.\u00a02758, pp. 75\u201393. Springer, Heidelberg (2003)"},{"key":"7_CR26","volume-title":"Narrative Intelligence: Papers from the AAAI Fall Symposium","author":"M. Schroeder","year":"1999","unstructured":"Schroeder, M.: How to tell a logical story. In: Narrative Intelligence: Papers from the AAAI Fall Symposium. AAAI Press, Menlo Park (1999)"},{"key":"7_CR27","volume-title":"Narrative Intelligence: Papers from the AAAI Fall Symposium","author":"R.M. Young","year":"1999","unstructured":"Young, R.M.: Notes on the use of plan structures in the creation of interactive plot. In: Narrative Intelligence: Papers from the AAAI Fall Symposium. AAAI Press, Menlo Park (1999)"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-22863-6_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,11,30]],"date-time":"2021-11-30T00:16:06Z","timestamp":1638231366000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-22863-6_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642228629","9783642228636"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-22863-6_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}