COMMENT ⊗   VALID 00008 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.REQUIRE "ABSTRA.CMD[BIB,CSR]" SOURCE FILE
C00003 00003	.once center <<general instructions>>
C00005 00004	%3STAN-CS-78-681  SET REPRESENTATION AND SET INTERSECTION
C00009 00005	%3STAN-CS-78-683  STORING A SPARSE TABLE
C00012 00006	%3STAN-CS-78-685  SPARSE AND PARALLEL MATRIX COMPUTATIONS
C00016 00007	%3AIM-315  PROLEGOMENA TO A THEORY OF FORMAL REASONING
C00020 00008	.NEXT PAGE
C00023 ENDMK
C⊗;
.REQUIRE "ABSTRA.CMD[BIB,CSR]" SOURCE FILE
.every heading (December Reports,,{Page})
.at "∞" ⊂"%4α∞%*"⊃
.next page
.once center <<general instructions>>
%3MOST RECENT CS REPORTS - DECEMBER 1978%1

@Listed below are abstracts of the most recent reports published by the Computer
Science Department of Stanford University.

@TO REQUEST REPORTS:##Check the appropriate places on the enclosed order form,
and return the entire order form page (including mailing label) by
December 4, 1978.
In many cases we can print only a limited number of copies, and requests will
be filled on a first come, first serve basis.  If the code (FREE) is printed
on your mailing label, you will not be charged for hardcopy.  This exemption
from payment is limited primarily to libraries.  (The costs shown include all
applicable sales taxes.  PLEASE SEND NO MONEY NOW, WAIT UNTIL YOU GET AN INVOICE.)

@ALTERNATIVELY:  Copies of most Stanford CS Reports may be obtained by writing
(about 2 months after MOST RECENT CS REPORTS listing) to NATIONAL TECHNICAL
INFORMATION SERVICE, 5285 Port Royal Road, Springfield, Virginia 22161.  Stanford
Ph.D. theses are available from UNIVERSITY MICROFILMS, 300 North Zeeb Road,
Ann Arbor, Michigan 48106.
.begin nofill
%4-------------------------------------------------------------------------------------%1
%3STAN-CS-78-681  SET REPRESENTATION AND SET INTERSECTION
%3Author:%1  Luis Trabb Pardo↔(Thesis)
.end
@%3Abstract:%1@This work discusses the representation and manipulation of sets
based on two different concepts:  tries, and hashing functions.

@The sets considered here are assumed to be static:  once created, there will
be no further insertions or deletions.  For both trie- and hash-based strategies,
a series of representation is introduced which together with the availability
of preprocessing reduces the average sizes of the sets to nearly optimal values,
yet retains the inherently good retrieval characteristics.

@The intersection procedure for trie-based representations is based on the
traversal in parallel of the tries representing the sets to be intersected, and
it behaves like a series of binary searches when the sets to be intersected are
of very different sizes.  Hashed intersection runs very fast.  The average time
is proportional to the size of the smallest set to be intersected and is
independent of the number of sets (except for the intersection set itself which
has to be checked for every set).
.break
.begin nofill
No. of pages:  85
Cost:  $ 4.10
%4-------------------------------------------------------------------------------------%1
%3STAN-CS-78-682  PARSING FLOWCHARTS AND SERIES-PARALLEL GRAPHS
%3Author:%1  Jacobo Valdes ↔(Thesis)
.end
@%3Abstract:%1@The main results presented in this work are an algorithm for the
recognition of General Series Parallel (GSP) digraphs and an approach to the
structural analysis of the control flow graphs of programs.

@The GSP recognition algorithm determines in %2O(n+m)%1 steps whether an acyclic
digraph with %2n%1 vertices and %2m%1 edges is GSP, and if it is, describes its
structure in terms of two simple operations on digraphs.  The algorithm is based
on the relationship between GSP digraphs and the more standard class of TTSP
multidigraphs.

@Our approach to the analysis of flow graphs uses the triconnected components
algorithm to find single-entry, single-exit regions.  Under certain
conditions -- that we identify -- this method will produce structural information
suitable for the global flow analysis of control flow graphs in time proportional
to the numer of vertices and edges of the graph being analyzed.
.break
.begin nofill
No. of pages:  233
Available in microfiche only.
%4-------------------------------------------------------------------------------------%1
%3STAN-CS-78-683  STORING A SPARSE TABLE
%3Author:%1  Robert Endre Tarjan
.end
@%3Abstract:%1@The problem of storing and searching large sparse tables arises
in compiling and in other areas of computer science.  The standard technique
for storing such tables is hashing, but hashing has poor worst-case performance.
We consider good worst-case methods for storing a table of %2n%1 entries, each
an integer between %2O%1 and %2N-1%1.  For dynamic tables, in which look-ups 
and table
additions are intermixed, the use of a trie requires %2O(kn)%1 storage and
allows %2O(log↓k(N/n))%1 worst-case access time, where %2k%1 is an arbitrary
parameter.  For static tables, in which the entire table is constructed before
any look-ups are made, we propose a method which requires %2O(n log∩[(l)]n)%1
storage and allow %2O(l log↓n N)%1 access time, where %2l%1 is an arbitrary
parameter.  Choosing %2l = log↑* n%1 gives a method with %2O(n)%1 storage and
%2O((log↑* n)(log↓n N))%1 access time.
.begin nofill
No. of pages:  23
Cost:  $ 2.35
%4-------------------------------------------------------------------------------------%1
%3STAN-CS-78-684  THE MATRIX INVERSE EIGENVALUE PROBLEM FOR PERIODIC JACOBI MATRICES
%3Authors:%1  D. L. Boley and G. H. Golub↔SU326 P30-64
.end
@%3Abstract:%1@A stable numerical algorithm is presented for generating a
periodic Jacobi matrix from two sets of eigenvalues and the product of the
off-diagonal elements of the matrix.  The algorithm requires a simple generalization
of the Lanczos algorithms.  It is shown that the matrix is not unique, but the
algorithm will generate all possible solutions.
.begin nofill
No. of pages:  18
Available in microfiche only.
%4-------------------------------------------------------------------------------------%1
%3STAN-CS-78-685  SPARSE AND PARALLEL MATRIX COMPUTATIONS
%3Author:%1  Franklin Tai-cheung Luk↔(Thesis)
.end
@%3Abstract:%1@This thesis deals with four important matrix problems:  (1) the
application of many variants of the conjugate gradient method for solving matrix
equations, (2) the solution of lower and upper bounds quadratic programs
associated with M-matrices, (3) the construction of a Block Lanczos method for
computing the greatest singular values of a matrix, and (4) the computation of
the singular value decomposition of a matrix of the ILLIAC-IV computer.
.begin nofill
No. of pages:  168
Available in microfiche only.
%4-------------------------------------------------------------------------------------%1
%3STAN-CS-78-686  EXTERNAL HASHING SCHEMES FOR COLLECTIONS OF DATA STRUCTURES
%3Author(s):%1  Richard J. Lipton, Arnold L. Rosenberg and Andrew C. Yao
.end
@%3Abstract:%1@We study the use of external hashing schemes for storing broad
classes of data structures.  Our general framework considers a class of data
structures partitioned into smaller classes by the number of positions in the
structure.  For instance, we could start with the class of all binary trees
and partition that class into the subclasses %2C%1↓1,%2C%1↓2,...%1 , each %2C↓n%1
comprising all %2n%1-node binary trees.  The main results establish
nonconstructively the existence of an external hashing scheme %2h↓n%1 with
%2O(n)%1 -storage demand and %2O(1)%1 -expected access time, that will store
any structure in %2C%1↓1%2α∪C%1↓2%2α∪...α∪C↓n%1 , provided %2C↓n%1 contains a number
of structures growing at most exponentially in %2n%1.  Classes of data
structures subsumed by these results include ragged arrays, binary trees,
string-indexed arrays, and refinable arrays.
.begin nofill
No. of pages:  33
Cost:  $ 2.65
%4-------------------------------------------------------------------------------------%1
%3AIM-315  PROLEGOMENA TO A THEORY OF FORMAL REASONING
%3Author:%1  Richard Weyhrauch
.end
@%3Abstract:%1@This paper is an introduction to the mechanization of a theory of
reasoning.  Currently formal systems are out of favor with the AI
community.  The aim of this paper is explain how formal systems can be
used in AI by explaining how traditional ideas of logic can be mechanized
in a practical way.  The paper presents several new ideas.  Each of these
is illustrated by giving simple examples of how this idea is mechanized in
the reasoning system FOL.  That is this is not just theory but there is an
existing running implementation of these ideas.

@In this paper: 1) we show how to mechanize the notion of model using the 
idea of a simulation structure and explain why this is particuliarly 
important to AI, 2) we show how to mechanize the notion of satisfaction, 
3) we present a very general evaluator for first order expressions, which 
subsumes PROLOG and we propose as a natural way of thinking about logic 
programming,  4) we show how to formalize metatheory,  5) we describe 
reflection principles, which connect theories to their metatheories in a 
way new to AI, 6) we show how these ideas can be used to dynamically 
extend the strength of FOL by "implementing" subsidiary deduction rules, 
and how this in turn can be extended to provide a method 
of describing and proving theorems about heuristics for using these rules, 
7) we discuss one notion of what it could mean for 
a computer to learn and give an example, 8) we describe a new kind of 
formal system tha has the property that it can reason about its own 
properties, 9) we give examples of all of the above.
.begin nofill
No. of pages:  41
Cost:  $ 2.85
%4-------------------------------------------------------------------------------------%1
%3AIM-318  SIX LECTURES ON THE LOGIC OF COMPUTER PROGRAMMING
%3Author:%1  Zohar Manna
.end
@%3Abstract:%1@These are notes from six tutorial lectures given at the NSF
Regional Conference, Renssellaer Polytechnic Institute, May 29-June 2, 1978.
The lectures deal with various aspects of the logic of computer programming:
.begin nofill; indent 5
partial correctness of programs
termination of programs
total correctness of programs
systematic program annotation
synthesis of programs
termination of production systems.
.end
.begin nofill
No. of pages:  54
Cost:  $ 3.25
%4-------------------------------------------------------------------------------------%1
.NEXT PAGE
%3AIM-319  AN %2n∩[log n]%3 ALGORITHM FOR THE TWO-VARIABLE-PER-CONSTRAINT LINEAR PROGRAMMING
			SATISFIABILITY PROBLEM
%3Author:%1  Charles G. Nelson
.end
@%3Abstract:%1@This paper describes a simple algorithm which determines the
satisfiability over the reals of a conjunction of linear inequalities, none of
which contains more than two variables.  In the worst case the algorithm requires
time %2O(mn∩[%5i%2log%1↓2%2n%5j%1+3]%1log%2n)%1, where %2n%1 is the number of
variables and %2m%1 is the number of constraints.  Several considerations
suggest that the algorithm may be useful in practice:  it is simple to implement,
it is fast for some important special cases, and if the constraints are
satisfiable it provides valuable information about the solution set of the
constraints.  The algorithm is particularly suited to applications in mechanical
verification.
.begin nofill
No. of pages:  20
Cost:  $ 2.30
%4-------------------------------------------------------------------------------------%1
%3AIM-320  A DEDUCTIVE APPROACH TO PROGRAM SYNTHESIS%1
%3Author:%1  Zohar Manna
.end
@%3Abstract:%1@Program synthesis is the systematic derivation of a program 
from given 
specifications.   A deductive approach to program synthesis is presented for
the construction of recursive programs.  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.
.begin nofill
No. of pages:  30
Cost:  $ 2.55
%4-------------------------------------------------------------------------------------%1
%4-------------------------------------------------------------------------------------%1