perm filename DEC.ABS[BIB,CSR] blob sn#389869 filedate 1978-10-19 generic text, type C, neo UTF8

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