QA4: A Procedural Calculus For Intuitive Reasoning

Abstract

This report presents a language, called QA4, designed to facilitate the construction of problem-solving systems used for robot planning, theorem proving, and automatic program synthesis and verification. QA4 integrates an omega-order logic language with canonical composition, associative retrieval, and pattern matching of expressions; process-structure programming; goal-directed searching; and demons. Thus it provides many useful programming aids. More importantly, however, it provides a semantic framework for common sense reasoning about these problem domains. The interpreter for the language is extraordinary general, and is therefore an adaptable tool for developing the specialized techniques of intuitive, symbolic reasoning used by the intelligence system. Chapter One is an informal introduction to the unusual programming concepts available in the QA4 language. Chapter Two is a primer for the language. It informally presents the language through the use of examples. Most of the unusual or complicated features of the language are not discussed. The chapter concludes with a presentation of a small robot planning system that uses only the language features presented in the chapter. Chapter Three presents a series of examples chosen to illustrate solutions to automatic programming problems. The QA4 programs used in Chapter Three rely on language features not presented in the primer. They are, however, explained as they occur. These programs illustrate most of the programming concepts just discussed. Chapter Four is a complete reference guide to the language. It provides the semantics of all the features of the language together with many implementation notes and design rationale. Chapter Five discusses extensions to the language that will probably be done during the next year.