Theorem proving and programming with dynamic first order logic

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 nondeterministic choice, and negation as (negated) test for continuation. We present a tableau style calculus for DFOL with explicit (simultaneous) substitution, prove its soundness and completeness, and point out its relevance for programming with dynamic first order logic, for automatic program analysis, and for semantics of natural language. Next, we extend this to an infinitary calculus for DFOL with iteration.