QA3 constructs solutions through proofs

An extended resolution procedure used proofs to construct solutions to formally described problems.

Cordell Green

AI topics

Explore related entries. Larger tags appear on more entries.

The contribution

Green connected theorem proving with finding an object or action sequence that satisfies a goal. QA3 used explicit descriptions of states and transformations, with demonstrations including small planning problems and simple program construction. This treated a proof as a route to a concrete solution, not just a yes-or-no answer.

What this does not establish

The examples required carefully specified axioms and restricted domains. They did not demonstrate reliable planning in an open, changing real-world environment.

Why this date?

1969 dates the IJCAI paper. The linked archive copy identifies itself as a preliminary version; SHRDLU reference 19 cites the conference work.

This entry follows the linked publication. Read the source and date conventions.

The original work

Application of Theorem Proving to Problem Solving

Authors: Cordell Green
Publication: IJCAI-69
Source type: Conference paper

Original IJCAI paper (PDF)

The links above support the description and dating of this entry. Full text may be open or publisher-restricted.

Cited By

Atlas entries whose reference lists cite this work or the publication version noted below.

Procedures as a Representation for Data in a Computer Program for Understanding Natural Language (1971)
Reference 19 cites Application of Theorem Proving to Problem Solving in the 1969 IJCAI proceedings. Check the reference list.

Citations

Works in the Atlas cited by this entry.

A Machine-Oriented Logic Based on the Resolution Principle (1965)
Listed in the source bibliography. Check the reference list.
The Use of Theorem-Proving Techniques in Question-Answering Systems (1968)
Listed in the source bibliography. Check the reference list.

Bibliography coverage: Reference section indexed. Open the source.

Reference text retains scan, spelling, line-break and column-order artifacts. Matching does not rely on publication year alone.

Read the indexed bibliography

Bibliography (PDF pages 19)

1. J. A. Robinson, "The Present State of Mechani c a l Theorem P r o v i n g , " a paper presented at the Fourth Systems Symposium, Cleveland, Ohio, November 19-20, 1968 (proceedings to be published). 2. C. Green and B. Raphael, "The Use of TheoremProving Techniques in Question-Answering Systems," Proc. 23rd N a t ' l . Conf. ACM, (Thompson Book Company, Washington, D.C., 1968). 3. C. Green, "Theorem Proving by Resolution as a Basis for Question-Answering Systems," Machine I n t e l l i g e n c e 4, D. Michie and B. Meltzer, Eds. (Edinburgh University Press, Edinburgh, Scotland, 1969). 4. N. J. Nilsson, "A Mobile Automaton: An A p p l i cation of A r t i f i c i a l Intelligence Techniques," a paper presented at the International Joint Conference on A r t i f i c i a l Intelligence, Washington, D.C., May 7-9, 1969 (proceedings to be published). 5. J. McCarthy and P. Hayes, "Some P h i l o s o p h i c a l Problems from the Standpoint of A r t i f i c i a l I n t e l l i g e n c e , " Machine I n t e l l i g e n c e 4, D. Michie and B. M e l t z e r , Eds. (Edinburgh U n i v e r sity Press, Edinburgh, Scotland, 1969). 6. R. J. Waldinger and R. C. T. Lee, "PROW: A Step Toward Automatic Program W r i t i n g , " a paper presented at the International Joint Conference on A r t i f i c i a l I n t e l l i g e n c e , Washi n g t o n , D.C., May 7-9, 1969 (proceedings to be published). 7. L. Wos, G. A. Robinson, and D. F. Carson, " E f f i c i e n c y and Completeness of the Set of Support Strategy in Theorem P r o v i n g , " J.ACM, V o l . 12, No. 4, pp. 536-541 (October 1965). 8. J. A. Robinson, "A Machine-Oriented Logic Based on the Resolution P r i n c i p l e , " J.ACM, V o l . 12, No. 1, pp. 23-41 (January 1965). 9. George E r n s t , " S u f f i c i e n t Conditions f o r the Success of GPS," Report No. SRC-68-17, Systems Research Center, Case Western Reserve U n i v e r s i t y , Celveland, Ohio (July 1968). 10. A. Hormann, "How a Computer System Can L e a r n , " IEEE Spectrum ( J u l y 1964). 1 1 . L. S. Coles, "Talking With a Robot in E n g l i s h , " paper submitted at the International Joint Conference on A r t i f i c i a l I n t e l l i g e n c e , Washi n g t o n , D.C., May 7-9, 1969 (proceedings to be published). 12. John McCarthy, Paul W. Abrahams, Daniel J. Edwards, Timothy P. H a r t , and Michael I. L e v i n , LISP 1.5 Programmer's Manual (The MIT Press, Cambridge, Mass., 1962). 13. C. Weissman, LISP 1.5 Primer (Dickenson Publ i s h i n g Company, I n c . , Belmont, C a l i f . , 1967). 14. Lawrence Wos and George Robinson, "Paramodul a t i o n and Set of S u p p o r t , " summary of paper presented at the IRIA Symposium on Automatic Demonstration at V e r s a i l l e s , France, December 1 6 - 2 1 , 1968 (proceedings to be p u b l i s h e d ) . 15. G. Robinson and L. Wos, "Paramodulation and Theorem-Proving in First-Order Theories with E q u a l i t y , " Machine I n t e l l i g e n c e 4, B. Meltzer and D. M i c h i e , Eds. (Edinburgh U n i v e r s i t y Press, Edinburgh, Scotland, 1969). 16. H. Simon, "Experiments w i t h a H e u r i s t i c Comp i l e r , " J.ACM, V o l . 10, pp. 493-506 (October 1963). 17. J. R. Slagle, "Experiments with a Deductive, Question-Answering Program," Comm. ACM, V o l . 8, pp. 792-798 (December 1965). 18. R. W. Floyd, "The V e r i f y i n g Compiler," Computer Science Research Review, Carnegie Mellon U n i v e r s i t y (December 1967). 19. z. Manna, "The Correctness of Programs," J. Computer and Systems Sciences, V o l . 3 (1969). 20. J. McCarthy, "Towards a Mathematical Science of Computation," Proceedings ICIP (North Holland P u b l i s h i n g Company, Amsterdam, 1962). 2 1 . B. Raphael, "A Computer Program Which 'Unders t a n d s ' , " Proc. FJCC, pp. 577-589 (1964). 22. W. S. Cooper, "Fact R e t r i e v a l and Deductive Question Answering Information Retrieval Systems," J.ACM, V o l . 1 1 , pp. 117-137 ( A p r i l 1964). 23. J. A. Robinson, "Mechanizing Higher Order L o g i c , " Machine I n t e l l i g e n c e 4, D. Michie and B. Meltzer, Eds. (Edinburgh University Press, Edinburgh, Scotland, 1969). 24. R. B. B a n e r j i , "A Language f o r Pattern Recogn i t i o n , " Pattern Recognition, V o l . 1, No. 1, pp. 63-74 (1968). 25. R. Kowalski, "The Case f o r Using E q u a l i t y Axioms in Automatic Demonstration," paper presented at the IRIA Symposium on Automatic Demonstration at V e r s a i l l e s , France, December 1 6 - 2 1 , 1968 (proceedings to be published) .

Download the bibliography index · Download Atlas citation links

These links cover verified matches within the Atlas. They are not total scholarly citation counts. A citation alone does not establish that the later system implements the same method.

AI topics

The contribution

What this does not establish

Why this date?

Comments