COMMENT ⊗   VALID 00019 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.require "setup.abs[bib,csr]" source file
C00004 00003	AIM-328
C00010 00004	STAN-CS-79-
C00011 00005	STAN-CS-79-
C00012 00006	STAN-CS-79-
C00013 00007	STAN-CS-79-
C00014 00008	STAN-CS-79-
C00015 00009	STAN-CS-79-
C00016 00010	STAN-CS-79-
C00017 00011	STAN-CS-79-
C00018 00012	STAN-CS-79-
C00019 00013	STAN-CS-79-
C00020 00014	STAN-CS-79-
C00021 00015	STAN-CS-79-
C00022 00016	STAN-CS-79-
C00023 00017	STAN-CS-79-
C00024 00018	STAN-CS-79-
C00025 00019	STAN-CS-79-
C00027 ENDMK
C⊗;
.require "setup.abs[bib,csr]" source file;
.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
@AGOAL:  A Goal Oriented Command Language for Interactive Proof Construction
Author:  Juan Bautista Bulnes-Rozas↔(Thesis)
   pages↔Cost: $
.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-

Author:  
   pages↔Cost: $
.end

.begin nofill
-↔-
STAN-CS-79-

Author:  
   pages↔Cost: $
.end

.begin nofill
-↔-
STAN-CS-79-

Author:  
   pages↔Cost: $
.end

.begin nofill
-↔-
STAN-CS-79-

Author:  
   pages↔Cost: $
.end

.begin nofill
-↔-
STAN-CS-79-

Author:  
   pages↔Cost: $
.end

.begin nofill
-↔-
STAN-CS-79-

Author:  
   pages↔Cost: $
.end

.begin nofill
-↔-
STAN-CS-79-

Author:  
   pages↔Cost: $
.end

.begin nofill
-↔-
STAN-CS-79-

Author:  
   pages↔Cost: $
.end

.begin nofill
-↔-
STAN-CS-79-

Author:  
   pages↔Cost: $
.end

.begin nofill
-↔-
STAN-CS-79-

Author:  
   pages↔Cost: $
.end

.begin nofill
-↔-
STAN-CS-79-

Author:  
   pages↔Cost: $
.end

.begin nofill
-↔-
STAN-CS-79-

Author:  
   pages↔Cost: $
.end

.begin nofill
-↔-
STAN-CS-79-

Author:  
   pages↔Cost: $
.end

.begin nofill
-↔-
STAN-CS-79-

Author:  
   pages↔Cost: $
.end

.begin nofill
-↔-
STAN-CS-79-

Author:  
   pages↔Cost: $
.end

.begin nofill
-↔-
STAN-CS-79-

Author:  
   pages↔Cost: $
.end

.begin nofill
-↔-