On July 19, 2016, Prof. Dr. Xishun Zhao (Sun Yat-sen University, Guangzhou) will give a talk about "Hoare style proof systems for plan verification under 0-approximation semantics" in the context of the SFB 901.
Abstract:
In this talk we would propose a Hoare style proof system called PR^0_D for plan verification under 0-approximation semantics of the action language A_K. In PR^0_D, a Hoare triple of the form {X}c{Y } means that all literals in Y become known to be true after executing plan c in a state in which all literals in X are known to be true. The proof systems are shown to be sound and complete, and more importantly, they give a way to efficiently generate and verify longer plans from existing verified shorter plans by applying so-called composition rule, provided that an enough number of shorter plans have been properly stored. The idea behind is a trade-off between space and time, we refer it to off-line planning and point out that it could be applied to general planning problems.