Structural Analysis of Narratives with the Coq Proof Assistant

DOI10.1007/978-3-642-22863-6_7zbMath1342.68280OpenAlexW4300749781WikidataQ57516617 ScholiaQ57516617MaRDI QIDQ3087995

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

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)

Related Items

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

Uses Software

• Coq
• Isabelle
• CiME
• A3PAT

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Linear logic
• Plans, actions and dialogues using linear logic
• Generating plans in linear logic. I: Actions as proofs
• Generating plans in linear logic. II: A geometry of conjunctive actions
• Narratives in the Situation Calculus
• A simple declarative language for describing narratives with actions