Logic & Formal Reasoning



QA4: A procedural calculus for intuitive reasoning

Classics

Abstract: This report presents a language, called QA4, designed to facilitate the construction of problem-solving systems used for robot planning, theorem proving, and automatic program synthesis and verification. Thus it provides many useful programming aids. More importantly, however, it provides a semantic framework for common sense reasoning about these problem domains. The interpreter for the language is extraordinarily general, and is therefore an adaptable tool for developing the specialized techniques of intuitive, symbolic reasoning used by the intelligent systems.


An approach to the frame problem, and its implementation

Classics

This paper proposes a method for handling the frame problem in representing conceptual, or natural-language-type information. The method is part of a larger calculus for expressing conceptual information, called P c F-2, which is described in Sandewall (1972), and which is a modification and extension of Sandewall (1971a). When the STRIPS schema adds a fact, PLANNER would add the corresponding fact to the data base using the primitive thassert. In this context, by epistemological information we mean a notation together with a set of rules (for example, logical axioms) which describe permissible deductions.


Computational logic: the unification computation

Classics

In designing an actual realization of the unification algorithm the first question which arises is how best to represent the expressions in the computer store. We have a collection of tables: symbol, args, vble, arity, subst, term, equals, and part, each of which has the same number N of rows. All the tables have one column, with the exception of args; and args has as many columns as the arity of that symbol, in the expressions being represented, whose arity is largest. We always arrange matters so that in a normal representation, distinct rows represent distinct expressions, i.e., so that We are now ready to explain the computation.


Question-answering in English

Classics

To illustrate how this may be done in very simple cases we give rules which translate certain declarative sentences and questions involving the quantifiers'some', 'every', 'any', and'no' into a modified first-order predicate calculus, and answer the questions by comparing their translated forms with those of the declaratives. John kissed Mary (1) Did John kiss Mary? (5) We begin by describing a method for translating a modest subset of English into a slightly modified first-order predicate calculus -- modified just enough to provide a representation for questions. We would like to have rules which transcribe such declarative sentences into predicate calculus formulae, such as VxMxj (7') 3x-- The matrix will be preceded by a string of quantifiers and negations -- and possibly a question mark; we have found that the transcription rules which appear below produce unique and acceptable orderings of these symbols from unambiguous sentences of the specified type.


Automatic Methods of Inductive Inference

Classics

This thesis is concerned with algorithms for generating generalisations-from experience. These algorithms are viewed as examples of the general concept of a hypothesis discovery system which, in its turn, is placed in a framework in which it is seen as one component in a multi-stage process which includes stages of hypothesis criticism or justification, data gathering and analysis and prediction. Formal and informal criteria, which should be satisfied by the discovered hypotheses are given. In particular, they should explain experience and be simple. The formal work uses the first-order predicate calculus. These criteria are applied to the case of hypotheses which are generalisations from experience. A formal definition of generalisation from experience, relative to a body of knowledge is developed and several syntactical simplicity measures are defined. This work uses many concepts taken from resolution theory (Robinson, 1965). We develop a set of formal criteria that must be satisfied by any hypothesis generated by an algorithm for producing generalisation from experience. The mathematics of generalisation is developed. In particular, in the case when there is no body of knowledge, it is shown that there is always a least general generalisation of any two clauses, in the generalisation ordering. (In resolution theory, a clause is an abbreviation for a disjunction of literals.) This least general generalisation is effectively obtainable. Some lattices induced by the generalisation ordering, in the case where there is no body of knowledge, are investigated. The formal set of criteria is investigated. It is shown that for a certain simplicity measure, and under the assumption that there is no body of knowledge, there always exist hypotheses which satisfy them. Generally, however, there is no algorithm which, given the sentences describing experience, will produce as output a hypothesis satisfying the formal criteria. These results persist for a wide range of other simplicity measures. However several useful cases for which algorithms are available are described, as are some general properties of the set of hypotheses which satisfy the criteria. Some connections with philosophy are discussed. It is shown that, with sufficiently large experience, in some cases, any hypothesis which satisfies the formal criteria is acceptable in the sense of Hintikka and Hilpinen (1966). The role of simplicity is further discussed. Some practical difficulties which arise because of Goodman's (1965) "grue" paradox of confirmation theory are presented. A variant of the formal criteria suggested by the work of Meltzer (1970) is discussed. This allows an effective method to be developed when this was not possible before. However, the possibility is countenanced that inconsistent hypotheses might be proposed by the discovery algorithm. The positive results on the existence of hypotheses satisfying the formal criteria are extended to include some simple types of knowledge. It is shown that they cannot be extended much further without changing the underlying simplicity ordering. A program which implements one of the decidable cases is described. It is used to find definitions in the game of noughts and crosses and in family relationships. An abstract study is made of the progression of hypothesis discovery methods through time. Some possible and some impossible behaviours of such methods are demonstrated. This work is an extension of that of Gold (1967) and Feldman (1970). The results are applied to the case of machines that discover generalisations. They are found to be markedly sensitive to the underlying simplicity ordering employed. Ph.D. thesis, Edinburgh University.


Natural language question-answering systems: 1969

Classics

In the meantime, Chomsky (1965) devised a paradigm for linguistic analysis that includes syntactic, semantic, and phonological components to account for the generation of natural language statements. This theory can be interpreted to imply that the meaning of a sentence can be represented as a semantically interpreted deep structure--i.e, From computer science's preoccupation with formal programming languages and compilers, there emerged another paradigm. The adoption and combination of these two new paradigms have resulted in a vigorous new generation of language processing systems characterized by sophisticated linguistic and logical processing of well-defined formal data structures. These included a social-conversation machine, systems that translated from English into limited logical calculi, and programs that attempted to answer questions from English text.


A note on mechanizing higher order logic

Classics

It seems most unlikely that one could in general write purely applicative Schonfmkel descriptions', like (5), of functions already known to one in some other form. One makes assertions in the system by writing clauses, i.e., finite collections of literals considered as disjunctions of their members, universally quantified with respect to all variables. In other words, this is a first-order language in which there is only one relation symbol, namely equality; only one function symbol, namely application; and a collection of individual constants. In particular the resolution principle may be used as sole principle; or the resolution principle together with paramodulation (Robinson and Wos 1969); or Sibert's system (Sibert 1969); or the E-resolution system of Morris (1969).


Planning and robots

Classics

Another substantial body of work on general problem-solving is that associated with the Graph Traverser program (Doran and Michie 1966, Doran 1967, Michie 1967, Doran 1968, Michie, Fleming and Oldfield 1968, Michie and Ross 1970). In this section and the next we shall consider the transition from heuristic problem-solving as exemplified by the Graph Traverser, to planning by a robot as exemplified by my own work and that of Marsh (Doran 1967, 1967a, 1968a, 1969; Marsh 1970; Michie 1967, 1968a; Popplestone 1967). In order to do this efficiently the program uses, in general, a heuristic state evaluation function and heuristic operator selection techniques to grow the search tree in the most promising direction. The following types of learning occurred in the system: (a) learning of the relationship between acts and perceptions by noting the effects of individual acts, by making generalizations about the effects of acts, and by noting that certain complicated transitions from one perceived state to another can always be achieved, (b) learning which acts to employ in particular situations and the benefits to be expected -- a kind of habit formation.


Some philosophical problems from the standpoint of artificial intelligence

Classics

We may regard the subject of artificial intelligence as beginning with Turing's article'Computing Machinery and Intelligence' (Turing 1950) and with Shannon's (1950) discussion of how a machine might be programmed to play chess. In this case we have to say that a machine is intelligent if it solves certain classes of problems requiring intelligence in humans, or survives in an intellectually demanding environment. However, we regard the construction of intelligent machines as fact manipulators as being the best bet both for constructing artificial intelligence and understanding natural intelligence. Given this notion of intelligence the following kinds of problems arise in constructing the epistemological part of an artificial intelligence: I.