This report describes a system of programs which perform natural

language processing based on an underlying language free

(conceptual) representation of meaning. This system is used to

produce sentence paraphrases which demonstrate a form of

understanding with respect to a given context. Particular emphasis

has been placed on the major subtasks of language analysis (mapping

natural language into conceptual structures) and language generation

(mapping conceptual structures into natural language), and on the

interaction between these processes and a conceptual memory model.

In visual-feedback work often a model of an object and its

approximate location are known and it is only necessary to determine

its location and orientation more accurately. The purpose of the

program described herein is to provide such information for the case

in which the model is an edge or corner. Given a model of a line or

a corner with two or three edges, the program searches a TV window

of arbitrary size looking for one or all corners which match the

model. A model-driven program directs the search. It calls on

another program to find all lines inside the window. Then it looks

at these lines and eliminates lines which cannot match any of the

model lines. It next calls on a program to form vertices and then

checks for a matching vertex. If this simple procedure fails, the

model-driver has two backup procedures. First it works with the

lines that it has and tries to form a matching vertex (corner). If

this fails, it matches parts of the model with vertices and lines

that are present and then takes a careful look in a small region in

which it expects to find a missing line. The program often finds

weak contrast edges in this manner. Lines are found by a global

method after the entire window has been scanned with the Hueckel

edge operator.

We present various heuristic techniques for use in proving the

correctness of computer programs. The techniques are designed to

obtain automatically the "inductive assertions" attached to the loops

of the program which previously required human "understanding" of the

program's approaches: one in which we obtain the inductive assertion

by analyzing predicates which are known to be true at the entrances

and exits of the loop (top-down approach), and another in which we

generate the inductive assertion directly from the statements of the

loop (bottom-up approach).

Defining the semantics of programming languages by axioms and rules

of inference yields a deduction system within which proofs may be

given that programs satisfy specifications. The deduction system

herein is shown to be consistent and also deductive complete with

respect to Hoare's sustem. A subgoaler for the deductive system is

described whose input is a significant subset of Pascal programs

plus inductive assertions. The output is a set of verification

conditions or lemmas to be proved. Several non-trivial arithmetic

and sorting programs have been shown to satisfy specifications by

using an interactive theorem prover to automatically generate prrofs

of the veification conditions. Additional components for a more

powerful verficiation system are under construction.

Signature table training method consists of cumulative evaluation of a

function (such as a probability density) at pre-assigned co-ordinate

values of input parameters to the table. The training is conditional:

based on a binary valued "learning" input to a table which is compared to

the label attached to each training sample. Interpretation of an unknown

sample vector is then equivalent of a table lookup, i.e. extraction of the

function value stored at the proper co-ordinates. Such a technique is

very useful when a large number of samples must be interpreted as in the case

of samples must be interpreted as in the case of speech recognition and the

time required for the trainng as well as for the recognition is at a premium.

However, this method is limited by prhibitive storage requirements, even for

a moderate number of parameters, when their relative independence cannot be

assumed. This report investigates the conditions under which the higher

dimensional probability density function can be decomposed so that the

density estimate is obtained by a hierarchy of signature tables with

consequent reduction in the storage requirement. Practical utility of the

theoretical results obtained in the report is demonstrated by a vowel

recognition experiment.