Verified synthesis of knowledge-based programs in finite synchronous environments

DOI10.1007/978-3-642-22863-6_9MaRDI QIDQ3087999zbMATH OpenOpenAlexFDO

Authors Peter Gammie

Publication date 17 August 2011

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

Full work available at URL https://doi.org/10.1007/978-3-642-22863-6_9

Mathematics Subject Classification ID

Logic in artificial intelligence (68T27) Agent technology and artificial intelligence (68T42)

Recommendations

• Knowledge-based synthesis of distributed systems using event structures
• Logic for Programming, Artificial Intelligence, and Reasoning
• Knowledge-based programs as plans. The complexity of plan verification
• scientific article; zbMATH DE number 2182499
• Knowledge-based programs

Cites work

• scientific article; zbMATH DE number 3670430 (Why is no real title available?)
• scientific article; zbMATH DE number 1512613 (Why is no real title available?)
• scientific article; zbMATH DE number 795590 (Why is no real title available?)
• Code generation via higher-order rewrite systems
• Computer Aided Verification
• Data Refinement
• Describing an algorithm by Hopcroft
• Formalizing the Logic-Automaton Connection
• General bindings and alpha-equivalence in Nominal Isabelle
• Interpretation of Locales in Isabelle: Theories and Proof Contexts
• Isabelle/HOL. A proof assistant for higher-order logic
• Logic for Programming, Artificial Intelligence, and Reasoning
• Multiagent Systems
• The Isabelle collections framework
• The dynamic logic of permission
• Verified synthesis of knowledge-based programs in finite synchronous environments

Cited in

(8)

• Finite state implementations of knowledge-based programs (extended abstract)
• Knowledge-based synthesis of distributed systems using event structures
• Knowledge-based programs as succinct policies for partially observable domains
• Logic for Programming, Artificial Intelligence, and Reasoning
• Interpreting knowledge-based programs
• Verified synthesis of knowledge-based programs in finite synchronous environments
• Knowledge-based programs as plans. The complexity of plan verification
• scientific article; zbMATH DE number 2182499 (Why is no real title available?)

Describes a project that uses

Uses Software

• Archive Formal Proofs
• Presburger Automata
• KBPs
• MCK
• MCMAS
• HOL
• VerICS
• Isabelle/HOL
• Isabelle

This page was built for publication: Verified synthesis of knowledge-based programs in finite synchronous environments

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