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
-↔-