Model verification and improvement using DISPROVER

摘要

Confidence in the adequacy of a model is increased if tasks that are impossible in the world are shown to correspond to disprovable tasks in the model. DISPROVER has been used as a tool to test, in worlds of robots, the impossibility of tasks related to various conservation laws (objects, position, model consistency, etc.) and time constraints. The adequacy and sufficiency of operators can be established. Interacting with DISPROVER, the model designer can improve his axiomatization.The frontier between “acceptable” and “ridiculous” axiomatizations is shown, in many examples, to be a most tenuous one.