This paper introduces a logic programming language called Demonic Dynamic Logic Programming. It is based on the ground, Demonic fragment of propositional dynamic logic, a well-studied program logic. Syntax, operational semantics and proof-theoretic semantics are presented. The theoretical foundations are validated by proving theorems such as soundness and existence of uniform proofs. Applications to two-player mathematical games are discussed and a pursuit-evasion game on a graph is presented as a concrete example. By bringing program logic and logic programming together, we hope to improve reasoning about imperative programs within logic programs. Future work is discussed, including extensions to game logic which hold the potential to generate winning strategies of games.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Demonic Dynamic Logic Programming

  • Rose Bohrer

摘要

This paper introduces a logic programming language called Demonic Dynamic Logic Programming. It is based on the ground, Demonic fragment of propositional dynamic logic, a well-studied program logic. Syntax, operational semantics and proof-theoretic semantics are presented. The theoretical foundations are validated by proving theorems such as soundness and existence of uniform proofs. Applications to two-player mathematical games are discussed and a pursuit-evasion game on a graph is presented as a concrete example. By bringing program logic and logic programming together, we hope to improve reasoning about imperative programs within logic programs. Future work is discussed, including extensions to game logic which hold the potential to generate winning strategies of games.