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.
A mature version of QLISP is described. QLISP permits free intermingling of advanced language constructs with those of INTERLISP. It provides an associative data base, viewed from perspectives controlled by a powerful context mechanism.
Earl D. Sacerdoti, Richard E. Fikes, Rene Reboh, Daniel Sagalowicz, Richard J. Waldinger, & B.M. Wilber
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.
Quantification in modal logic is interesting from a technical and philosophical stand-point. Here we look at quantification in auto-epistemic logic, which is a modal logic of self-knowledge.
In 1981 SRI introduced RANSAC, a now widely referenced paradigm for robust communication ideally suited to computer vision (a type of artificial intelligence used in image analysis.
This paper derives the basis of a theory of communication from a formal theory of rational interaction. The major result is a demonstration that illocutionary acts need neither be primitive, nor explicitly recognized.
This paper describes research concerned with automating the monitoring and control of spacecraft systems. In particular, the paper examines the application of SRI’s Procedural Reasoning System (PRS) to the handling of malfunctions in the Reaction Control System (RCS) of NASA’s space shuttle
Expert systems that operate in complex domains are continually confronted with the problem of deciding what to do next. Being able to reach a decision requires, in part, having the capacity to "reason" about a set of alternative actions.
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.
