Structural analysis of narratives with the Coq proof assistant

DOI10.1007/978-3-642-22863-6_7MaRDI QIDQ3087995zbMATH OpenOpenAlexDBLPWikidataFDO

Authors Anne-Gwenn Bosser, Pierre Courtieu, Julien Forest, Marc Cavazza

Publication date 17 August 2011

Published in Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL https://research.tees.ac.uk/en/publications/813c661d-f423-4ed8-ad31-b53da2d22919

zbMATH Keywords

linear logicapplications of theorem proversformal models of narratives

Mathematics Subject Classification ID

Logic in artificial intelligence (68T27) Proof-theoretic aspects of linear logic and other substructural logics (03F52)

Recommendations

• Linear Logic for non-linear storytelling
• Proof assistants for natural language semantics
• Narrative Structure of Mathematical Texts
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Interactive proofs in higher-order concurrent separation logic

Cites work

• scientific article; zbMATH DE number 4055576 (Why is no real title available?)
• scientific article; zbMATH DE number 786489 (Why is no real title available?)
• A simple declarative language for describing narratives with actions
• Generating plans in linear logic. I: Actions as proofs
• Generating plans in linear logic. II: A geometry of conjunctive actions
• Linear Logic for non-linear storytelling
• Linear logic
• Narratives in the Situation Calculus
• Plans, actions and dialogues using linear logic

Cited in

(20)

• A formal semantics of nested atomic sections with thread escape
• Verifying relative safety, accuracy, and termination for program approximations
• A realizability interpretation of Church's simple theory of types
• Formalizing Soundness of Contextual Effects
• Proofs, programs, processes
• Explaining Gabriel-Zisman localization to the computer
• Some aspects of narrative method
• An effective proof of the well-foundedness of the multiset path ordering
• Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme
• Targeted configuration of an SMT solver
• Experimenting Formal Proofs of Petri Nets Refinements
• Linear Logic for non-linear storytelling
• Automated verification of the parallel Bellman-Ford algorithm
• Regular language representations in the constructive type theory of Coq
• Local Termination
• Proof assistants: history, ideas and future
• TPS: A hybrid automatic-interactive system for developing proofs
• Executing and verifying higher-order functional-imperative programs in Maude
• An introduction to univalent foundations for mathematicians
• Lem: a lightweight tool for heavyweight semantics

Describes a project that uses

Uses Software

• A3PAT
• CiME
• Isabelle
• Coq

This page was built for publication: Structural analysis of narratives with the Coq proof assistant

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3087995)