Deduction-Based Refinement Planning

Weintroduce a method of deduction-based refinement planning where prefabricated general solutions are adapted to special problems. Refmementproceeds by stepwise transforming nonconstructive problem specifications into executable plans. For eachrefinementstep there is a correctness proof guaranteeing the soundnessof refinement and with that the generation of provably correct plans. Bysolving the hard deduction onceand for all on the abstract level, planning on the concrete level becomesmoreefficient. Withthat, our approachaims at making deductiveplanningfeasible in realistic contexts. Ourapproachis based on a temporallogic frameworkthat allows for the representation of specifications and plans onthe samelinguistic level. Basicactions andplans are specified using a programminglanguage the constructs of which are formulaeof the logic. Abstractsolutions are represented as--possibly recursive--procedures. It is this commonlevel of representation and the fluid transition betweenspecificatio...

• Type: Conference
• Year: 1996
• Where: AIPS
• Authors: Werner Stephan, Susanne Biundo
• Keywords: AIPS 1996, Artificial Intelligence, Deduction-based Refinement, Executable Plans, Nonconstructive Problem Specifications