A Deductive Approach to Automated Planning

The principal goal of this project is to apply techniques from automated deduction to programs in real-world and robotic planning and the synthesis of imperative programs. Expected benefits include a reduction in the human effort required to develop complex plans and programs, a reduction in the err...

Full description

Saved in:
Bibliographic Details
Main Author: Waldinger, Richard J
Format: Report
Language:English
Subjects:
ALGORITHMS
ARTIFICIAL INTELLIGENCE
AUTOMATION
Cybernetics
EQUATIONS
FRAMES
LPN-SRI17784
MATHEMATICAL LOGIC
PLANNING
PROBLEM SOLVING
RECURSIVE FUNCTIONS
ROBOTICS
ROBOTS
SYNTHESIS
THEORY
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:The principal goal of this project is to apply techniques from automated deduction to programs in real-world and robotic planning and the synthesis of imperative programs. Expected benefits include a reduction in the human effort required to develop complex plans and programs, a reduction in the error-rate associated with planning and programming, and an increase in the ease of modifying existing plans and programs to accommodate to changes in purpose and environment. In this document problems in commonsense and robot planning are approached by methods adapted from program synthesis research; planning is regarded as an application of automated deduction. To support this approach, the authors introduce a variant of situational logic, called plan theory, in which plans are explicit objects. A machine-oriented deductive-tableau inference system is adapted to plan theory. Equations and equivalences of the theory are built into a unification algorithm for the system. Frame axioms are built into the resolution rule. Special attention is paid to the derivation of conditional and recursive plans. Inductive proofs of theorems for even the simplest planning problems, such as clearing a block, have been found to require challenging generalizations.