Tableau reasoning and programming with dynamic first order logic
Jan van Eijck · Logic Journal of IGPL · 2001
Dynamic First Order Logic (DFOL) 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) 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. Next, we extend this to an infinitary calculus for DFOL with iteration and connect up with other work in dynamic logic.