A mechanized framework for specifying problem domains and verifying plans
Sakthikumar Subramanian · 1993
This dissertation presents a framework for modeling problem domains in the Boyer-Moore logic so that we can verify mechanically solutions to various problems using the Boyer-Moore theorem prover. A problem domain is given by a set of states of the physical world and a set of actions that can be executed sequentially to change state. A problem is given by an initial condition and a goal condition. A solution is a plan that when executed in a state satisfying the initial condition will bring about a goal state. We are mainly interested in verifying plans that involve conditional and repetitive actions for solving problems in domains such as the blocks world. Such domains arise in both artificial intelligence and software engineering. Our main contribution is a method of specifying problem domains in the Boyer-Moore logic for verifying plans interactively. We illustrate our method by verifying plans for solving problems in some variations of the blocks world. We show how solutions to problems in a class of domains can be verified using the n x n mutilated checkerboard problem. Our method of specifying domains does not suffer from many of the limitations of current approaches such as the need for stating explicitly a large number of separate frame axioms and state constraints necessary for reasoning about actions with side-effects. Our formalization also allows us to express many other properties of plans such as efficiency requirements. Because both specifications and plans are executable, we can prove properties about them in logic as well as test them on concrete data. Our method can also be used to obtain a formalization that would enable a program to verify plans depending on changes to domain specifications received as input at various times. Non-monotonic formalisms have generally been used for this purpose but have proven difficult to implement. We illustrate our approach by mechanizing reasoning about actions described in the language ${\cal A}$.