Author: Richard J. Waldinger

The paper considers how such algorithms might be derived from their specifications by an automatic program-synthesis system. The derivation of the binary-search concept has been found to be surprisingly straightforward.

TABLOG (Tableau Logic Programming Language) is a language based on first-order predicate logic with equality that combines functional and logic programming. TABLOG incorporate advantages of LISP and PROLOG.

The task of deriving a unification algorithm automatically is beyond the power of existing program synthesis systems. We will identify some of the capabilities required of a theorem-proving system to perform this derivation automatically.

This approach regards program synthesis as a theorem-proving task and relies on a theorem-proving method that combines the features of transformation rules, unification, and mathematical induction within a single framework.

Techniques derived from mathematical logic promise to provide an alternative to the conventional methodology for constructing, debugging, and optimizing computer programs. This paper provides a unified tutorial exposition of the logical techniques, illustrating each with examples.

This approach, which we call the intermittent-assertion method, involves documenting the program with assertions that must be true at some time when control is passing through the corresponding point, but that need not be true every time.

This paper presents a functional overview of the features and capabilities of QLISP, one of the newest of the current generation of very high level languages developed for use in artificial intelligence (AI) research.

This paper develops the following strategy: to achieve two goals simultaneously, develop a plan to achieve one of them and then modify that plan to achieve the second as well. A systematic program modification technique is presented to support this strategy.

We describe some of the reasoning and programming capabilities of a projected synthesis system with special attention paid to the introduction of conditional tests, loops, and instructions with wide effects in the program being constructed.

This paper describes a theorem prover that embodies knowledge about programming constructs, such as numbers, arrays, lists, and expressions. The program can reason about these concepts and is used as part of a program verification system that uses the Floyd-Naur explication of program semantics.

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.