C. Hewitt, PLANNER: A Language for Proving Theorems in Robots. International Joint Conference on Artificial Intelligence, 1969.

Author of the summary: J. William Murdock, 1997, murdock@cc.gatech.edu

Cite this paper for:

• Difficult problems require more sophisticated knowledge representations than "finite-state difference tables of connections between goals and methods."

Keywords: Theorem Proving, Representation, Pattern Matching,
Goal, Logic, Backtracking

Systems: PLANNER

Summary: Provides a language for theorem proving.  Nominally oriented
toward robotics, this paper doesn't seem to say much that is
particular to this field.  Talks about the relationship between
declarative and imperative information.  For example "(implies $_a
$_b)" is a logical assertion but also is associated with several
actions such as "If we want to deduce $$b, then establish a subgoal to
first deduce $$a."

Summary author's notes:

• This summary came from a file which had the following disclaimer: "The following summaries are the completely unedited and often hastily composed interpretations of a single individual without any sort of systematic or considered review. As such it is very likely that at least some of the following text is incomplete, inadequate, misleading, or simply wrong. One might view this as a very preliminary draft of a survey paper that will probably never be completed. The author disclaims all responsibility for the accuracy or use of this document; this is not an official publication of the Georgia Institute of Technology or the College of Computing thereof, and the opinions expressed here may not even fully match the fully considered opinions of the author much less the general opinions of the aformentioned organizations."