The strategy has been implemented in a simple QLISP program.

This is the second of two papers about MOLGEN.

No part of this publication may be reproduced, stored in a retrieval system, or transmitted, in any form or by any means--electronic, mechanical, photocopying, recording, or otherwise--without the prior written permission of the publisher.

Instead they have commonly assigned structure to a domain using statistical techniques such as Bayes' Theorem

ABSTRACT Deductive question-answering systems generally evaluate queries under one of two possible assumptions which we in this paper refer to as the open and closed world assumptions. The open world assumption corresponds to the usual first order approach to query evaluation: Given a data base DB and a query Q, the only answers to Q are those which obtain from proofs of Q given DB as hypotheses. Under the closed world assumption, certain answers are admitted as a result of failure to find a proof. More specifically, if no proof of a positive ground literal exists, then the negation of that literal is assumed true. In this paper, we show that closed world evaluation of an arbitrary query may be reduced to open world evaluation of socalled atomic queries. We then show that the closed world assumption can lead to inconsistencies, but for Horn data bases no such inconsistencies can arise. Finally, we show how for Horn data bases under the closed world assumption purely negative clauses are irrelevant for deductive retrieval and function instead as integrity constraints. INTRODUCTION Deductive question-answering systems generally evaluate queries under one of two possible assumptions which we in this paper refer to as the open and closed world assumptions.

The first section discusses the importance of having systems that own M.S. thesis (Moore, 19)5), suggests that predicate calculus can understand the concept of knowledge, and how knowledge is be treated in a more natural manner than resolution and related to action. Section 2 points out some of the special problems combined with domain-dependent control information for greater that are involved in reasoning about knowledge, and section $ efficiency. Furthermore, the problems of reasoning about knowledge seem to require the full ability to handle quantifiers presents a logic of knowledge based on the idea of possible worlds. Section 4 integrates this with a logic of actions and gives an and logical connectives which only predicate calculus posseses.

We learn (memorize) multiplication tables, learn (discover how) to walk, learn (build UP an understanding of, then an ability to synthesize) languages. Many subtasks and capabilities are involved in these various kinds of learning. One capability central to many kinds of learning is the ability to generalize: to take into account a large number of specific observations, then to extract and retain the important common features that characterize classes of these observations. This generalization problem has received considerable attention for two decades in the fields of Artificial Intelligence, Psychology, and Pattern Recognition (e.g., [Bruner, 1956],

The extensions are heuristically non-trivial, because the equivalent In (McCarthy and Hayes 1969), we proposed dividing the predicate calculus may be much longer and is usually much more artificial intelligence problem into two parts - an epistemological difficult to understand - for man or machine.

Circumscription formalizes such conjectural reasoning.

Program synthesis is the systematic derivation of a program from a given specification. A deductive approach to program synthesis is presented for the construction of recursive programs. This approach regards program synthesis as a theorem-proving task and relies on a theorem-proving method that combines the features of transformation rules, unification, and mathematical induction within a single framework. MOTIVATION The early work in program synthesis relied strongly on mechanical theoremproving techniques. The work of Green [5] and Waldinger and Lee [13], for example, depended on resolution-based theorem proving; however, the difficulty of representing the principle of mathematical induction in a resolution framework hampered these systems in the formation of programs with iterative or recursive loops. More recently, program synthesis and theorem proving have tended to go their separate ways. Newer theorem-proving systems are able to perform proofs by mathematical induction (e.g., Boyer and Moore [2]) but are useless for program synthesis because they have sacrificed the ability to prove theorems involving existential quantifiers. In this paper we describe a framework for program synthesis that again relies on a theorem-proving approach. This approach combines techniques of unification, mathematical induction, and transformation rules within a single deductive system. We outline the logical structure of this system without considering the strategic aspects of how deductions are directed. Although no implementation exists, the approach is machine oriented and ultimately intended for implementation in automatic synthesis systems. In the next section we give examples of specifications accepted by the system. In the succeeding sections we explain the relation between theorem proving and our approach to program synthesis. SPECIFICATION The specification of a program allows us to express the purpose of the desired program, without indicating an algorithm by which that purpose is to be achieved.