Author: Richard J. Waldinger
-
A Language for Writing Problem-Solving Programs
This paper describes a language for constructing problem-solving programs that can manipulate several data structures, including ordered and unordered sets.
-
On Program Synthesis and Program Verification
Certain similarities between program verification and program synthesis are pointed out. The analogy is illustrated using a “bubble-sort” program.
-
Towards Automatic Program Synthesis
An elementary outline of the theorem-proving approach to automatic program synthesis is given, without dwelling on technical details.
-
Robot Problem Solving* Without State Variables
Waldinger has proposed a scheme for getting around the original robot problem by extending the logic to handle sets and tuples (still keeping an explicit state variable around).
-
Pointing to Places in a Deductive Geospatial Theory
Issues in the description of places are discussed in the context of a logical geospatial theory.
-
Deductive Coordination of Multiple Geospatial Knowledge Sources
This theory lies at the core of the system GeoLogica, which deduces answers to geographical questions based on knowledge provided by multiple agents.
-
Research in Advanced Formal Theorem-Proving Techniques
This report summaries the results of a three-year project aimed at the design and implementation of computer languages to aid in expressing problem solving procedures in several areas of artificial intelligence including automatic programming, theorem proving, and robot planning.