| Combination and Interoperation of Logical Systems Research in Formal Interoperability |
30 APR 1999 |
10 pages |
| Authors:
John McCarthy; Carolyn Talcott; STANFORD UNIV CA DEPT OF COMPUTER SCIENCE
|
 | This project involved investigation of both interpretations of the phrase formal interoperability: (1) formal semantics of the interoperation of components and their combination into complex systems; and (2) the interoperation of formal systems and their combined use to specify the many aspects of complex systems. (1) scientific foundations for sensible, correct and secure interaction between components; (2) formalizing different aspects of complex systems and ... |
|
| Basic Research in Knowledge Representation |
01 MAY 1998 |
7 pages |
| Authors:
John McCarthy; Carolyn Talcott; STANFORD UNIV CA DEPT OF COMPUTER SCIENCE
|
| This project concerned developing new logical formalisms for representing information. New formalisms allow us to represent information that we previously could not capture. New reasoning methods allow us to integrate more information and can yield conclusions that were previously unavailable. One basic method that was developed involves introducing contexts as mathematical objects and developing formal language for describing the relations between sentences true in different contexts. This allows information that ... |
|
| A Statistical Characterization of Denver-Area Microbursts. Revision |
DEC 92 |
55 pages |
| Authors:
Kimberly L. Elmore; John McCarthy; NATIONAL CENTER FOR ATMOSPHERIC RESEARCH BOULDER CO
|
| This document describes statistical characteristics of microbursts that occurred in the Denver area during the summers of 1982 and 1984. The Joint Airport Weather Studies (JAWS) Project, conducted between 15 May and 13 August 1982, is the primary data source for this report, and radar data from the Classify, Locate and Avoid Wind Shear (CLAWS) Project are also included for microburst lines and low-reflectivity microbursts. All surface mesonet data come ... |
|
| Common Prototyping Language |
AUG 91 |
126 pages |
| Authors:
John McCarthy; STANFORD UNIV CA DEPT OF COMPUTER SCIENCE
|
| Prototyping is the process of writing programs for the purpose of obtaining information prior to constructing a production version. Prototyping is used to increase the probability that the first production version will be satisfactory. It is thus a tool for reducing risk. Prototyping differs from production programming in that efficiency and completeness are often sacrificed in the interests of rapid development and ease of obtaining information. At present there is ... |
|
| Open Architecture for Formal Reasoning |
AUG 91 |
5 pages |
| Authors:
John McCarthy; STANFORD UNIV CA DEPT OF COMPUTER SCIENCE
|
| This task represents an initial part of a long term project aimed at making both theoretical and practical advances in the field of formal reasoning. The main goal is to provide a framework for designing and experimenting with symbol manipulation programs, and in particular, to provide a general software architecture for implementing formal reasoning systems and interfaces to existing software components including special purpose theorem provers, program transformers, and databases. ... |
|
| Mathematical Theory of Computation |
AUG 91 |
8 pages |
| Authors:
John McCarthy; STANFORD UNIV CA DEPT OF COMPUTER SCIENCE
|
| This project was concerned with the development of correct and reusable software through the use of higher order abstractions (function, control, assignment, process) and reflection. A semantic framework for these notions will be the basis of an experimental system for manipulating and reasoning about programs. The goals of this project were the development of logical formalisms for reasoning about programs that use abstractions and reflection, and the application of these ... |
|
| QLISP for Parallel Processors |
NOV 90 |
7 pages |
| Authors:
John McCarthy; STANFORD UNIV CA DEPT OF COMPUTER SCIENCE
|
| Stanford University has completed the initial phase of the Qlisp project for research on parallel Lisp programming. The research made use of the Qlisp implementation on the Alliant FX/8 delivered by Lucid, Inc. under subcontract to Stanford University. The results we have obtained confirm, in general, our predictions that a shared-memory multiprocessor is an effective tool for executing symbolic programs in Lisp. The major highlights of Qlisp have been: 1) ... |
|
| A Statistical Characterization of Denver-Area Microbursts |
MAR 89 |
55 pages |
| Authors:
Kimberly L. Elmore; John McCarthy; NATIONAL CENTER FOR ATMOSPHERIC RESEARCH BOULDER CO
|
| This document describes statistical characteristics of microbursts that occurred in the Denver area during the summers of 1982 and 1984. The Joint Airport Weather Studies (JAWS) Project, conducted between 15 May and 13 August 1982, is the primary data source for this report, and radar data from the Classify, Locate and Avoid Wind Shear (CLAWS) Project are also included for microburst lines and low-reflectivity microbursts. All surface mesonet data come ... |
|
| QLISP for Parallel Processors |
JAN 89 |
4 pages |
| Authors:
John McCarthy; STANFORD UNIV CA DEPT OF COMPUTER SCIENCE
|
| The goal of the Qlisp project at Stanford is to gain experience with the shared-memory, queue-based approach to parallel Lisp, by implementing the Qlisp language on an actual multiprocessor, and by developing a symbolic algebra system as a testbed application. The experiments performed on the simulator included: 1. Algorithms for sorting and basic data structure manipulation for polynomials. 2. Partitioning and scheduling methods for parallel programming. 3. Parallelizing the production ... |
|
| Basic Research in Artificial Intelligence and Foundations of Programming. |
MAY 1980 |
|
| Authors:
John McCarthy; Thomas Binford; David Luckham; Zohar Manna; Richard Weyhrauch; STANFORD UNIV CA DEPT OF COMPUTER SCIENCE
|
 | This report describes recent research in several related areas. Basic research in artificial intelligence and formal reasoning addresses fundamental problems in the representation of knowledge and reasoning processes applied to this knowledge. Solution of these problems will make possible the development of analytical applications of computers with large and complex data bases, where current systems can handle only a very restricted set of data structures and queries. Mathematical theory of ... |
|
| Ascribing Mental Qualities to Machines. |
MAR 1979 |
|
| Authors:
John McCarthy; STANFORD UNIV CALIF DEPT OF COMPUTER SCIENCE
|
| Ascribing mental qualities like beliefs, intentions and wants to a machine is sometimes correct if done conservatively and is sometimes necessary to express what is known about its state. We propose some new definitional tools for this: definitions relative to an approximate theory and second order structural definitions. (Author) |
|
| First Order Theories of Individual Concepts and Propositions. |
MAR 1979 |
|
| Authors:
John McCarthy; STANFORD UNIV CALIF DEPT OF COMPUTER SCIENCE
|
| We discuss first order theories in which individual concepts are admitted as mathematical objects along with the things that reify them. This allows very straightforward formalizations of knowledge, belief, wanting, and necessity in ordinary first order logic without modal operators. Applications are given in philosophy and in artificial intelligence. (Author) |
|
| Recursive Programs as Functions in a First Order Theory. |
MAR 1979 |
|
| Authors:
Robert Cartwright; John McCarthy; STANFORD UNIV CALIF DEPT OF COMPUTER SCIENCE
|
| Pure Lisp style recursive function programs are represented in a new way by sentences and schemata of first order logic. This permits easy and natural proofs of extensional properties of such programs by methods that generalize structural induction. It also systematizes known methods such as recursion induction, subgoal induction, inductive assertions by interpreting them as first order axiom schemata. We discuss the metatheorems justifying the representation and techniques for proving ... |
|
| Recent Research in Artificial Intelligence and Foundations of Programming. |
SEP 1978 |
|
| Authors:
John McCarthy; Tom Binford; Cordell Green; David Luckham; Zohar Manna; STANFORD UNIV CALIF DEPT OF COMPUTER SCIENCE
|
| This report summarizes recent research in the following areas: artificial intelligence and formal reasoning, mathematical theory of computation and program synthesis, program verification, image understanding, and knowledge based programming. (Author) |
|
| On the Model Theory of Knowledge. |
APR 1978 |
|
| Authors:
John McCarthy; Masahiko Sato; Takeshi Hayashi; Shigeru Igarashi; STANFORD UNIV CALIF DEPT OF COMPUTER SCIENCE
|
| Another language for expressing 'knowing that' is given together with axioms and rules of inference and a Kripke type semantics. The formalism is extended to time-dependent knowledge. Completeness and decidability theorems are given. The problem of the wise men with spots on their foreheads and the problem of the unfaithful wives are expressed in the formalism and solved. (Author) |
|
| Recent Research in Computer Science. |
JUN 1977 |
|
| Authors:
John McCarthy; Thomas Binford; Cordell Green; David Luckham; Zohar Manna; STANFORD UNIV CALIF DEPT OF COMPUTER SCIENCE
|
| This report summarizes recent accomplishments in six related areas: basic AI research and formal reasoning, image understanding, mathematical theory of computation, program verification, natural language understanding, and knowledge based programming. |
|
| Three Reviews of J. Weizenbaum's Computer Power and Human Reason. |
NOV 1976 |
|
| Authors:
Bruce G. Buchanan; Joshua Lederberg; John McCarthy; STANFORD UNIV CALIF DEPT OF COMPUTER SCIENCE
|
| Three reviews of J. Weizenbaum's Computer Power and Human Reason (W. H. Freeman and Co., San Francisco, 1976) are reprinted from other sources. A reply by Weizenbaum to McCarthy's review is also reprinted. (Author) |
|
| Project Technical Report, |
MAR 1971 |
82 pages |
| Authors:
John McCarthy; Arthur Samuel; Edward Feigenbaum; Joshua Lederberg; STANFORD UNIV CALIF DEPT OF COMPUTER SCIENCE
|
| An overview is presented of current research at Standford in artificial intelligence and heuristic programming. This report is largely the text of a proposal to the Advanced Research Projects Agency for fiscal years 1972-3. (Author) |
|
| STANFORD ARTIFICIAL INTELLIGENCE PROJECT. |
APR 1970 |
|
| Authors:
John McCarthy; Edward Felgenbaum; Joshua Lederberg; STANFORD UNIV CALIF DEPT OF COMPUTER SCIENCE
|
| Current research is reviewed in artificial intelligence and related areas, including representation theory, mathematical theory of computation, models of cognitive processes, speech recognition, and computer vision. (Author) |
|
| PROPERTIES OF PROGRAMS AND PARTIAL FUNCTION LOGIC, |
OCT 1969 |
|
| Authors:
Zohar Manna; John McCarthy; STANFORD UNIV CALIF DEPT OF COMPUTER SCIENCE
|
| Recursive definitions are considered which consist of Algol-like conditional expressions. By specifying a computation rule for evaluating such recursive definition, it determines a partial function. However, for different computation rules, the same recursive definition may determine different partial functions. Two types of computation rules are distinguished: sequential and parallel. The purpose of the paper is to formalize properties (such as termination, correctness and equivalence) of these partial functions by means ... |
|
| PROJECT TECHNICAL REPORT, |
JUN 1969 |
|
| Authors:
John McCarthy; STANFORD UNIV CALIF DEPT OF COMPUTER SCIENCE
|
| Plans and accomplishments of the Stanford Artificial Intelligence Project are reviewed in several areas including: theory (epistemology and mathematical theory of computation), visual perception and control (Hand-eye and Cart), speech recognition by computer, heuristics in machine learning and automatic deduction, models of cognitive processes (Heuristic DENDRAL, Language Research, and Higher Mental Functions). (Author) |
|
| SOME PHILOSOPHICAL PROBLEMS FROM THE STANDPOINT OF ARTIFICIAL INTELLIGENCE, |
04 NOV 1968 |
|
| Authors:
John McCarthy; Patrick Hayes; STANFORD UNIV CALIF DEPT OF COMPUTER SCIENCE
|
| A computer program capable of acting intelligently in the world must have a general representation of the world in terms of which its inputs are interpreted. Designing such a program requires commitments about what knowledge is and how it is obtained. Thus some of the major traditional problems of philosophy arise in artificial intelligence. The first part of the paper begins with a philosophical point of view that seems to ... |
|
| PROJECT TECHNICAL REPORT, |
13 SEP 1968 |
|
| Authors:
John McCarthy; Edward Feigenbaum; Arthur Samuel; STANFORD UNIV CALIF DEPT OF COMPUTER SCIENCE
|
| Recent work of the Stanford Artificial Intelligence Project is summarized in several areas: Scientific hypothesis formation; Symbolic computation; Hand-eye systems; Computer recognition of speech; Board games; and Other projects. (Author) |
|
| CORRECTNESS OF A COMPILER FOR ARITHMETIC EXPRESSIONS. |
29 APR 1966 |
|
| Authors:
John McCarthy; James Painter; STANFORD UNIV CALIF DEPT OF COMPUTER SCIENCE
|
| The paper contains a proof of the correctness of a simple compiling algorithm for compiling arithmetic expressions into machine language. |
|
| Problems in the Theory of Computation, |
11 MAY 1965 |
|
| Authors:
John McCarthy; STANFORD UNIV CALIF DEPT OF COMPUTER SCIENCE
|
| The purpose of this paper is to identify and discuss a number of theoretical problems whose solutions seems feasible and likely to advance the practical art of computation. (Modified author abstract) |
|
| Plans for the Stanford Artificial Intelligence Project, |
20 APR 1965 |
|
| Authors:
John McCarthy; STANFORD UNIV CALIF DEPT OF COMPUTER SCIENCE
|
| The paper discusses the proposals of the contract which are to obtain: A computer-controlled eye that a computer can use to get a picture into computer memory for processing; A computer controlled hand that can be programmed to assemble an object out of parts; and A computer suitable for controlling these things and also suitable for providing symbolic computation for the other artificial intelligence projects which are being undertaken. |
|
| A Proof-Checker for Predicate Calculus, |
03 MAR 1965 |
|
| Authors:
John McCarthy; STANFORD UNIV CALIF DEPT OF COMPUTER SCIENCE
|
| A program that checks proofs in J. A. Robinson's formulation of predicate calculus has been programmed in LISP 1.5. The program is available in CTSS at Project MAC and is also available as a card deck. The program is used for class exercises at Stanford. (Author) |
|
| A Formal Description of a Subset of Algol, |
24 SEP 1964 |
|
| Authors:
John McCarthy; STANFORD UNIV CALIF DEPT OF COMPUTER SCIENCE
|
| The author describes Microalgol, a trivial subset of ALGOL, by means of an interpreter. The notions of abstract syntax and of state of the computation permit a compact description of both syntax and semantics. The author advocates an extension of this technique as a general way of describing programming languages. (Modified author abstract) |
|
| A Tough Nut for Proof Procedures, |
17 JUL 1964 |
|
| Authors:
John McCarthy; STANFORD UNIV CALIF DEPT OF COMPUTER SCIENCE
|
| It is well known to be impossible to tile with dominoes a checkerboard with two opposite corners deleted. This fact is readily stated in the first order predicate calculus, but the usual proof which involves a parity and counting argument does not readily translate into predicate calculus. It is conjectured that this problem will be very difficult for programmed proof procedures. (Modified author abstract) |
|
| Computer Control of a Machine for Exploring Mars, |
15 JUN 1964 |
|
| Authors:
John McCarthy; STANFORD UNIV CALIF DEPT OF COMPUTER SCIENCE
|
| Landing a 5000 pound package on Mars that would spend a year looking for life and making other measurements has been proposed. It is believed that this machine should be a stored program computer with sense and motor organs, and that the machine should be mobile. The author discusses the following points: Advantages of a computer controlled system; what the computer should be like; what we can feasibly program the ... |
|
| Programs with Common Sense, |
18 SEP 1963 |
|
| Authors:
John McCarthy; STANFORD UNIV CALIF DEPT OF COMPUTER SCIENCE
|
| This paper discusses programs to manipulate in a suitable formal language (most likely a part of the predicate calculus) common instrumental statements. The basic program will draw immediate conclusions from a list of premises. These conclusions will be either declarative or imperative sentences. When an imperative sentence is deduced the program takes a corresponding action. These actions may include printing sentences, moving sentences on lists, and reinitiating the basic deduction ... |
|
| Situations, Actions, and Causal Laws, |
03 JUL 1963 |
13 pages |
| Authors:
John McCarthy; STANFORD UNIV CALIF DEPT OF COMPUTER SCIENCE
|
| A formal theory is given concerning situations, causality and the possibility and effects of actions is given. The theory is intended to be used by the Advice Taker, a computer program that is to decide what to do by reasoning. Some simple examples are given of descriptions of situations and deductions that certain goals can be achieved. (Author) |
|
| Predicate Calculus with 'Undefined' as a Truth-Value, |
22 MAR 1963 |
|
| Authors:
John McCarthy; STANFORD UNIV CALIF DEPT OF COMPUTER SCIENCE
|
| The author would like to use predicate calculus in the mathematical theory of computation. In particular, the author would like to write formulas involving recursively defined predicates and functions. The trouble is that recursively defined predicates are not guaranteed to be defined for all values of their arguments, and therefore, it is not clear how to interpret formulas involving them. The author gives an interpretation of predicate calculus formulas involving ... |
|
Reports by Author
