Programming with dynamic predicate logic

We propose to bring together two research traditions, computation with first order logic from computer science, and dynamic interpretation of first order logic from natural language semantics. We define a new executable process interpretation for first order logic, and show that it is a faithful approximation of the dynamic interpretation procedure for first order formulas. We then demonstrate the dynamic logic programming alternative to destructive assignment and show how to obtain a versatile logic programming language by adding constructs for bounded choice and for bounded and unbounded iteration. Finally, we show that the operational semantics for first order logic given in Apt and Bezem cite{AptBezem:fap is an approximation of our executable semantics. It follows that the operational semantics is faithful to the dynamic interpretation of first order logic. Our results relate a recent turn in executable computational interpretation of FOL formulas to a research tradition from natural language semantics, and suggest a new paradigm of dynamic logic programming that combines imperative power with dynamic declarative semantics.