Proof System for Plan Verification under 0-Approximation Semantics

TL;DR

This paper introduces a proof system for verifying plans under 0-approximation semantics in knowledge-based action theories, ensuring correctness and completeness for plan verification and generation.

Contribution

It develops a sound and complete proof system for plan verification under 0-approximation semantics, enabling plan verification and generation in knowledge-based systems.

Findings

Proof system is sound and complete.

Enables plan verification under 0-approximation semantics.

Supports plan generation based on the proof system.

Abstract

In this paper a proof system is developed for plan verification problems $\{X\}c\{Y\}$ and $\{X\}c\{KW p\}$ under 0-approximation semantics for ${\mathcal A}_K$. Here, for a plan $c$, two sets $X,Y$ of fluent literals, and a literal $p$, $\{X\}c\{Y\}$ (resp. $\{X\}c\{KW p\}$) means that all literals of $Y$ become true (resp. $p$ becomes known) after executing $c$ in any initial state in which all literals in $X$ are true.Then, soundness and completeness are proved. The proof system allows verifying plans and generating plans as well.