Goto

Collaborating Authors

 Logic & Formal Reasoning


10 On Representations of Problems of Reasoning about Actions Saul Amarel

AI Classics

The general problem of re-Presentation is concerned with the relationship between different ways of formulating a problem to a problem solving system and the efficiency with which the system can be expected to find a solution to the problem. An understanding of the relationship between problem formulation and problem solving efficiency is a prerequisite for the design of procedures that can automatically choose the most appropriate' representation of a problem (they can find a point of view' of the problem that maximally simplifies the process of finding a solution). Many problems of practical importance are problems of reasoning about actions. In these problems, a course of action has to be found that satisfies a number of specified conditions. A formal definition of this class of problems is given in the next section, in the context of a general conceptual framework for formulating these problems for computers. Everyday examples of reasoning about actions include planning an airplane trip, organizing a dinner party, etc. There are many examples of industrial and military problems in this category, such as scheduling assembly and transportation processes, designing a program for a computer, planning a military operation, etc. The research presented in this paper was sponsored in part by the Air Force Office of Scientific Research, under Contract Number A F49(638)-1184. Part of this work was done while the author was on a visiting appointment at the Computer Science Department of the Carnegie Institute of Technology, Pittsburgh, Pa.



THE RESOLUTION PRINCIPLE IN THEOREM-PROVING

AI Classics

INTRODUCTION The evidence is already in favour of the computer becoming an aid to research in branches of mathematics which do not involve numerical computation. Programs have now been constructed for performing certain symbolic operations in mathematics, for example algebraic simplification of equations and indefinite integration, and for solving some of the problems (which are certainly not in the class of numerical calculations) now occurring in theoretical physics and other areas. One may reasonably expect that sooner or later programs of this type will be incorporated in a'questionanswering' package. As the construction of multi-programming systems progresses, and'on-line' use of the computer is accepted as normal, it will become more and more practicable for the mathematician to rely on the computer for answers to routine non-numerical questions. It is, therefore, of interest from a practical as well as a theoretical point of view to ask if this development can be taken a stage further by mechanising the processes of mathematical proof. In this way the computer could be used as a tool for establishing true mathematical statements or checking proofs for correctness. The problem is essentially to produce practicable programs for proving theorems which will answer some reasonably complicated questions before overstepping the bounds of available time and memory space. This is potentially one of the most rewarding areas of computer applications, but as many people already know, it is also one of the most frustrating.


BETH-TREE METHODS IN AUTOMATIC THEOREM-PROVING

AI Classics

In the'condition omitted' column: denotes that the full complement of heuristic devices was in use denotes that the coefficient of the feature L was set to zero denotes that the coefficient of the feature B was set to zero de,notes that the coefficient of the feature E was set to zero denotes that the coefficient of the feature T was set to zero PD denotes that all neighbours of a node were produced at one development M denotes that the example group was not in use 44 POPPLESTONE F denotes that the equality was proved in reverse, i.e., that the RHS was converted into the LHS. Note that the LHS is longer than the RHS in every problem where the lengths are different. In the'result' column: S denotes that the problem was solved F denotes that the problem was unsolved after 100 distinct nodes had been produced - FF denotes that the problem was unsolved after 100 distinct nodes had been produced but that the problem was solved after restarting one or more times from the most promising node produced so far (see Doran's paper in this volume). FL denotes that the problem was unsolved because a term too large to hold in the array assigned to hold it was produced. The nodes listed' column gives the total number of distinct nodes produced.


Report 85-19 Evaluating the Existing Tools for Developing

AI Classics

In recent years there has been a great deal of interest in the commercial applications of knowledge-based (KB) systems (commonly called expert systems). Interest in KB systems was spurred on by the development of programs that can solve complex tasks at an expert level.


Report 85-12 The Complete Guide to MRS

AI Classics

MRS stands for Meta-level Representation System. If your response to this is a knowing nod of understanding you can probably skip the first few chapters. In a sense, MRS is a computer language, in that one enters text in a designated syntax and it gets processed and produces answers (or not). But because MRS is also able to reason with the information you give it, the'program' you enter can be seen more as representing facts than specifying a process. The importance and utility of this difference will become clear.


RESIDUE A Deductive Approach to Design Synthesis

AI Classics

We present a new approach to deductive design synthesis, the Residue Approach, in which designs are represented as sets of constraints. Previous approaches, such as PROLOG [181 or the work of Manna and WaWinger [111, express designs as bindings on single terms. We give a complete and sound procedure for Ending sets of propositions constituting a legal design. The size of the search space of the procedure and the advantages and disadvantages of the Residue Approach are analysed. In particular we show how Residue can avoid backtracking caused by making design decisions of overly coarse granularity. In contrast, it is awkward for the single term approaches to do the same. In addition we give a rule for constraint propagation in deductive synthesis, and show its use in pruning the design space. Finally, Residue is related to other work, in particular, to Default Logic [16] and to Assumption-Based Truth Maintenance [1].


Artificial intelligence: Toward Machines that Think

AI Classics

Stanford -- KSL that Think. Consideration of the of the new 16-bit integrated circuits that phenomenal progress of the past 30 years leaves one with a feeling of have allowed computers oi small size and considerable power to be developed. The only certainty in sight is that scientists. BRUCE G. BUCHANAN is Professor of In addition to game playing early Al work focused on techniques for solving Computer Science Research at Stanford small symbolic reasoning problems. Researchers continue to ponder these problems (Overleat) Illustration by f red Nelson as well.


Report 84 01 Partial Programs . Stanford Michael R. Nov 1984

AI Classics

A complete program is one that for any environment specifies a unique action for a machine to perform. Programs in most traditional programming languages are complete in this sense. By contrast, a partial program is merely an arbitrary set of constraints on the potential actions of a machine and does not necessarily specify a unique action in every enviranment.