Sound and Complete Calculus for Update Logic

摘要

A sound and complete deduction system for Veltman's update logic in the style ofthe Hoare calculus with two kinds of correctness statements for dynamic assignment logic in Van Eijck and De Vries is presented. The Hoare correctness statements use modal propositional logic assertion language and connect update logic to the modal propositional logic S5. The connection with modal propositional logic provides a clear link between the dynamic and the static semantics of update logic. Update logic is already noted to be decidable; S5 provides an alternative proof. The S5 connection can also be used for rephrasing the validity notions of update logic and for performing consistency checks.