COIS 140a Project: PDL in Prolog

PDL is a relatively recent (first formulated in the late 1970s) outgrowth of modal logic and Floyd-Hoare logic. Essentially, it uses modal operators over computations to express, for instance, that after performing some operation a, some proposition φ holds. Its original intent was to provide a way of reasoning about program behavior (and it still has applications in this area), but has more recently been applied to AI systems and autonomous agents.

The implementation consists of an interpreter and a model file (model 1, model 2). Please read the documentation for instructions and discussion.

References

• The Wikipedia article provides a decent, high-level introduction to the subject.
• The Gamut of Dynamic Logics, by Jan van Eijck and Martin Stokhof provides a longer, and much more in-depth look at PDL.
• Propositional Dynamic Logic of Regular Programs (M.J. Fischer & R.E. Ladner, 1979) is one of the seminal papers on the topic.
• Dynamic Logic (Harel, et al. 1984), is an excellent introductory article on the subject. It was later expanded into a book of the same name (MIT Press, 2000).