Author: Richard J. Waldinger

They may reside on different machines in diverse locations. Knowledge may be represented according to different frameworks, notations, or coordinate systems. The answer may not exist anywhere explicitly; it may need to be inferred, and it may depend on more than one source

We present our vision of a DAML-enabled search architecture; a set of queries of increasing complexity that should be answered efficiently in a Semantic Web.

In this paper, we focus on the process of reuse and report a case study on constructing a KB by reusing existing knowledge. The reuse process involved the following steps: translation, comprehension, slicing, reformulation, and merging.

Snark, SRI’s New Automated Reasoning Kit, is a theorem prover intended for applications in artificial intelligence and software engineering. This document is an example-driven tutorial introduction to snark that will allow the reader to experiment with the system.

The goal of this project was to enable knowledge engineers to construct knowledge bases (KBs) faster. To achieve this goal, we investigated two techniques: knowledge reuse and axiom templates. The results were demonstrated by developing a question-answering system for the crisis management challenge problem (CMCP).

The heart of the system is a knowledge base (KB) and a collection of reasoning methods. The KB is being constructed by a combination of manual and semiautomatic methods. The reasoning methods include conventional database query processing, frame-based reasoning, and full first-order theorem proving.

Automated deduction techniques are being used in a system called Amphion to derive, from graphical specifications, programs composed from a subroutine library. The system has been applied to construct software for the planning and analysis of interplanetary missions.

Book available online

An informal tutorial is presented for program synthesis, with an emphasis on deductive methods. According to this approach, to construct a program meeting a given specification, we prove the existence of an object meeting the specified conditions.

Deductive methods are being applied to their validation, to detect flaws in these systems and enable us to use them with more confidence. Each system of rules is encoded as a set of axioms that define the system theory.

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.