近年来关于不完全知识的规划成为活跃的研究领域,许多逻辑系统引入感知动作、条件规划描述这一问题。作为代表性的成果之一,Son和Baral提出了动作语言Ak及其不完全信息下的推理语义。本研究进一步为Ak设计了谨慎语义和弱谨慎语义,使得主体可以在严格安全环境下生成并执行可靠的规划。计算复杂性分析表明谨慎语义降低了Ak的推理复杂性;为上述语义提出用于验证条件规划推理机制的Hoare型证明系统,该系统是可靠和完全的,既可应用于规划生成,又可应用于规划验证;且该系统有离线规划的性质,即在离线状态下主体可以将已有的短的证明组成新的长的证明。