perm filename FIVE[BIB,CSR]3 blob sn#453032 filedate 1979-07-02 generic text, type C, neo UTF8

COMMENT ⊗ VALID 00006 PAGES C REC PAGE DESCRIPTION C00001 00001 C00002 00002 .require "setup.abs[bib,csr]" source file C00003 00003 .begin center C00005 00004 AIM-328 C00011 00005 STAN-CS-79-744↔CSL TR-172 C00017 00006 STAN-CS-79-745 C00033 ENDMK C⊗; .require "setup.abs[bib,csr]" source file; .at "⊗" ⊂"%5αQ%*"⊃ .at "!!" txt ";" ⊂ .("txt"[1]&"∩[%2"&"txt"[2]&"]&∪[ "&"txt"[3]&"]"); . ⊃ .begin center S T A N F O R D U N I V E R S I T Y MOST RECENT COMPUTER SCIENCE REPORTS - 1979 .end .begin nofill No. 4↔August -↔- -↔- .end @Listed here are abstracts of the most recent reports published by the Department of Computer Science at 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 October 26, 1979. 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 the 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. .skip .begin nofill -↔- -↔- AIM-328 @GOAL: A Goal Oriented Command Language for Interactive Proof Construction Author: Juan Bautista Bulnes-Rozas↔(Thesis) 175 pages↔Available in microfiche only. .end @This thesis represents a contribution to the development of practical computer systems for interactive construction of formal proofs. Beginning with a summary of current research in automatic theorem proving, goal oriented systems, proof checking, and program verification, this work aims at bridging the gap between proof checking and theorem proving. @Specifically, it describes a system GOAL for the First Order Logic proof checker FOL. GOAL helps the user of FOL in the creation of long proofs in three ways: 1) as a facility for structured, top down proof construction; 2) as a semi-automatic theorem prover; and 3) as an extensible environment for the programming of theorem proving heuristics. @In GOAL, the user defines top level goals. These are then recursively decomposed into subgoals. The main part of a goal is a well formed formula that one desires to prove, but they include assertions, simplification sets, and other information. Goals can be tried by three different types of elements: %2matchers%1, %2tactics%1, and %2strategies%1. @The %2matchers%1 attempt to prove a goal directly -that is without reducing it into subgoals- by calling decision procedures of FOL. Successful application of a matcher causes the proved goal to be added to the FOL proof. @A %2tactic%1 reduces a goal into one or more subgoals. Each tactic is the inverse of some inference rule of FOL; the goal structure records all the necessary information so that the appropriate inference rule is called when all the subgoals of a goal are proved. In this way the goal tree unwinds automatically, producing a FOL proof of the top level goal from the proofs of its leaves. @The %2strategies%1 are programmed sequences of applications of tactics and matchers. They do not interface with FOL directly. Instead, they simulate a virtual user of FOL. They can call the tactics, matchers, other strategies, or themselves recursively. The success of this approach to theorem proving success is documented by one heuristic strategy that has proved a number of theorems in Zermelo-Fraenkel Axiomatic Set Theory. Analysis of this strategy leads to a discussion of some trade offs related to the use of %2assertions%1 and %2simplification sets%1 in goal oriented theorem proving. @The user can add new tactics, matchers, and strategies to GOAL. These additions cause the language to be extended in a uniform way. The description of new strategies is done easily, at a fairly high level, and no faulty deduction is possible. Perhaps the main contribution of GOAL is a high level environment for easy programming of new theorem proving applications in the First Order Predicate Calculus. @The thesis ends with two appendixes presenting complete proofs of Ramsey's theorem in axiomatic Set Theory and of the correctness of the Takeuchi function. @(It is planned that both FOL and GOAL will be made available over the ARPANET this year. Inquiries regarding their use should be addressed to Dr. R. Weyhrauch at the Stanford Artificial Intelligence Laboratory, SU-AI). .begin nofill -↔- STAN-CS-79-744↔CSL TR-172 @PERFORMANCE OF UPDATE ALGORITHMS FOR REPLICATED DATA IN A DISTRIBUTED DATABASE Author: Hector Garcia-Molina↔(Thesis) 320 pages↔Cost: $6.20 .end @In this thesis we study the performance of update algorithms for replicated data in a distributed database. In doing so, we also investigate several other related issues. @We start by presenting a simple model of a distributed database which is suitable for studying updates and concurrency control. We also develop a performance model and a set of parameters which represent the most important performance features of a distributed database. @The distributed database models are used to study the performance of update algorithms for replicated data. This is done in two steps. First the algorithms are analyzed in the case of completely replicated databases in a no failure, update only environment. Then, the restrictions that we made are eliminated one at a time, and the impact on the system performance of doing this is evaluated. For the first step, we develop a new technique for analyzing the performance of update algorithms. This iterative technique is based on queueing theory. Several well known update algorithms are analyzed using this technique. The performance results are verified through detailed simulations of the algorithms. The results show that centralized control algorithms nearly always perform better than the more popular distributed control algorithms. This is a surprising result because the distributed algorithms were thought to be more efficient. @The performance results are also useful for identifying the critical system resources. This insight leads to the development of several new update algorithms with improved performance. In particular, the MCLA-h algorithms which we present performs better than all other update algorithms in most cases of interest. The MCLA-h algorithm is based on the new concept that "hole lists" which are used to increase the parallelism of updates. Several varations of the MCLA-h algorithms are also analyzed. @In order to investigate the validity of our results in a general system, we relax the assumptions made initially in the performance studies. We show that it is @possible to make a centralized control algorithm (like the MCLA-h) resilient in the face of many types of failures. We show that the cost in terms of performance fordoing this is roughly the same for all algorithms and thus, the original performance comparisons are still valid in the case of crash resistant algorithms. @We analyze distributed databases with partitioned data and multiple independent control mechanisms (called controllers). We describe transaction processing in this environment and we discuss how the performance results of the fully duplicated case can be used to design update algorithms in this environment. @We demonstrate how updates that do not specify their base set initially can be processed. We present three fundamental alternatives for processing these updates and we analyze their performance. @The operation of read only transactions (queries) and their interaction with the update algorithms has not been covered in the literature. In this thesis, we classify queries to free, consistent and current queries, and we present algorithms for processing each type of query under the different update algorithms. .begin nofill -↔- STAN-CS-79-745 @UPPER AND LOWER BOUNDS ON TIME-SPACE TRADEOFFS IN A PEBBLE GAME Author: Thomas Lengauer↔(Thesis) 83 pages↔Cost: $4.05 .end @We derive asymptotically tight time-space tradeoffs for pebbling three different classes of directed acyclic graphs. Let %2N%1 be the size of the graph, %2S%1 the number of available pebbles, and %2T%1 the time necessary for pebbling the graph. @(a) A time-space tradeoff of the form .once center %2ST = ⊗(N↑2)%1 is proved for pebbling (using only black pebbles) a special class of permutation graphs that implement the bit reversal permutation. If we are allowed to use black and white pebbles the time-space tradeoff is shown to be of the form .once center %2T = !!⊗NS; + ⊗(N)%1. @(b) A time-space tradeoff of the form .once center %2T = S !!⊗NS;)∩[!!⊗NS;]%1 is proved for pebbling a class of graphs constructed by stacking superconcentrators in a series. This time-space tradeoff holds whether we use only black or black and white pebbles. @(c) A time-space tradeoff of the form .once center %2T = S 2∩[2∩[!!⊗NS;]]%1 is proved for pebbling general directed acyclic graphs with only black or black and white pebbles. .begin nofill -↔-