Abstract

Dynamic First Order Logic results from interpreting quantification over a variable v as change of valuation over the v position, conjunction as sequential composition, disjunction as non-deterministic choice, and negation as test for continuation. We present a tableau style calculus for DFOL with explicit binding, prove its soundness and completeness, and point out its relevance for programming with DFOL, for automated program analysis including loop invariant detection, and for semantics of natural language. We also extend this to an infinitary calculus for DFOL with iteration and connect up with other work in dynamic logic