Demonic Dynamic Logic Programming
摘要
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.