perm filename FIVE[BIB,CSR]2 blob sn#450694 filedate 1979-06-21 generic text, type C, neo UTF8

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