返回Google圖書搜尋

A Sound and Complete Calculus for Update Logic

出版	Centre for Mathematics and Computer Science, 1991
URL	http://books.google.com.hk/books?id=oiGXRAAACAAJ&hl=&source=gbs_api

註釋Abstract: "This paper presents a sound and complete deduction system for Veltman's update logic in the style of the Hoare calculus with two kinds of correctness statements for dynamic assignment logic in Van Eijck and De Vries [13]. The Hoare correctness statements use modal propositional logic as 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. The fact that update logic is decidable was noted already in [10]; the connection with 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."