A mechanized framework for specifying problem domains and verifying plans

摘要: 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 theorem prover. A domain is given by set of states physical world and actions be executed sequentially change state. an initial condition goal condition. solution plan when state satisfying will bring about We are mainly interested verifying plans involve conditional repetitive solving such as blocks world. Such arise both artificial intelligence software engineering. Our main contribution method specifying interactively. illustrate our some variations show how class verified n x mutilated checkerboard problem. Our does not suffer from many limitations current approaches need stating explicitly large number separate frame axioms constraints necessary reasoning with side-effects. formalization also allows us express other properties efficiency requirements. Because specifications executable, prove them well test on concrete data. Our used obtain would enable program depending changes received input at times. Non-monotonic formalisms have generally been this purpose but proven difficult implement. approach mechanizing described language ${\cal A}$.