Logic & Formal Reasoning
The complexity of theorem-proving procedures
It is shown that any recognition problem solved by a polynomial time-bounded nondeterministic Turing machine can be "reduced" to the problem of determining whether a given propositional formula is a tautology. Here "reduced" means, roughly speaking, that the first problem can be solved deterministically in polynomial time provided an oracle is available for solving the second. From this notion of reducible, polynomial degrees of difficulty are defined, and it is shown that the problem of determining tautologyhood has the same polynomial degree as the problem of determining whether the first of two given graphs is isomorphic to a subgraph of the second. A method of measuring the complexity of proof procedures for the predicate calculus is introduced and discussed.
A Paradigm for Reasoning by Analogy
A paradigm enabling heuristic problem solving programs to exploit an analogy between a current unsolved problem and a similar but previously solved problem to simplify it s search for a solution is outlined. It is developed in detail for a first-order resolution logic theorem prover. Descriptions of the paradigm, implemented LISP programs, and preliminary experimental results are presented. This is believed to be the firs t system that develops analogical information and exploits it so that a problem-solving program can speed its search.IJCAI-71, British Computer Society, London, 1971. Revised version in Artificial intelligence 2(2):147- 178, fall, 1971.
STRIPS: A New Approach to the Application of Theorem Proving to Problem Solving
Reprinted in Readings in Planning, edited by J. Allen, J. Hendler, and A. Tate, Morgan Kaufmann Publishers, San Mateo, California, 1990. Also Reprinted in Computation and Intelligence: Collected Readings, edited by George F. Luger, AAAI Press, 1995. See also: Artificial Intelligence, Volume 2, Issues 3–4, Winter 1971, Pages 189–208 In IJCAI-71: INTERNATIONAL JOINT CONFERENCE ON ARTIFICIAL INTELLIGENCE. British Computer Society, London.. Revised version in Artificial Intelligence, 2(3), pp 189-208.
A Further Note on Inductive Generalization
In this paper, we develop the algorithm, given in Plotkin (1970), for findingthe least generalization of two clauses, into a theory of inductive generalization.The types of hypothesis which can be formed are very simple. They allhave the form: (x)Px --> Qx.We have been guided by ideas from the philosophy of science, followingBuchanan (1966). There is no search for infallible methods of generatingtrue hypotheses. Instead we define (in terms of first-order predicate calculus)the notions of data and evidence for the data. Next, some formal criteria areset up for a sentence to be a descriptive hypothesis which is a good explanationof the data, given the evidence. We can then look for the best such hypothesis.Machine Intelligence 6
Question-answering in English
Isard, S. | Longuet-Higgins, H.C.
The problem we consider in this paper is that of discovering formal ruleswhich will enable us to decide when a question posed in English can beanswered on the basis of one or more declarative English sentences. Toillustrate how this may be done in very simple cases we give rules whichtranslate 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 ofthe declaratives. We suggest that in order to capture the meanings of morecomplex sentences it will be necessary to go beyond the first-order predicatecalculus, to a notation in which the scope of words other than quantifiersand negations is clearly indicated.Machine Intelligence 6