Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Gazing: An approach to the problem of definition and lemma use

  • Published:
Journal of Automated Reasoning Aims and scope Submit manuscript

Abstract

A major outstanding problem in automated theorem proving research is determining the appropriate use of definitions and previously proved theorems within a proof. Presenting the theorem prover with only the formulae that are necessary for the proof might be viewed as ‘cheating’ and requires that the user prove the theorem ahead of time. In real world applications of theorem proving, this is almost certain to be infeasible. On the other hand providing the prover with all formulae that might be relevant rapidly swamps the prover with unnecessary information. A technique for the selective retrieval of formulae based on features of those formulae and the conjecture at hand is required to solve this problem.

In this paper I describe an abstraction-based technique which addresses this problem. Implicit hypotheses such as definitions, axioms and previously proved theorems are stored in a database which may be accessed by a heuristic rule of inference calledgazing. Before accessing this database the gazing rule plans the use of these formulae in a hierarchy of abstraction spaces. When the planning phase is complete, the system can use the indicated formulae with some confidence that they are relevant to the proof.

Since the technique is abstraction-based, no guarantee that the plant will be eventually applicable or successful can be made. However, because the plans are built by considering increasing amounts of detail, the number of ways in which the application of a plan can fail is limited. Plan failures may be ‘patched’ in a uniform way.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

Explore related subjects

Discover the latest articles, news and stories from top researchers in related subjects.

References

  1. Bledsoe, W. W., ‘The UT interactive prover’, Memo ATP-17B, Mathematics Department, University of Texas, April 1983.

  2. Bledsoe, W. W. and Tyson, M., ‘The UT interactive prover’, Memo ATP-17, Mathematics Department, University of Texas, May 1975.

  3. Boyer, R. S. and Moore, J. S.,A Computational Logic. ACM Monograph Series, Academic Press, 1979.

  4. Bundy, A., ‘Finding a common currency — a new proof plan’. Internal Note 159, Department of Artificial Intelligence, University of Edinburgh, January 1983.

  5. CvetkovicD. and PevacI., ‘Man-machine theorem proving in graph theory’,Artificial Intelligence 35, 1–23 (1988).

    Article  MathSciNet  Google Scholar 

  6. FikesR. E., HartP. E., and NilssonN. J., ‘Learning and executing generalized robot plans’,Artificial Intelligence 3, 251–288 (1972).

    Article  Google Scholar 

  7. FikesR. E. and NilssonN. J., ‘Strips: A new approach to the application of theorem proving to problem solving’,Artificial Intelligence 2, 189–208 (1971).

    Article  Google Scholar 

  8. Halmos, P.,Naive Set Theory. Van Nostrand. 1960.

  9. Kleene, S. C.,Mathematical Logic, John Wiley and Sons, Inc., 1967.

  10. Minsky, M., ‘Steps towards artificial intelligence’, in:Computers and Thought, McGraw Hill, 1963, pp. 406–450.

  11. Plaisted, D. A., ‘Abstraction mappings in mechanical theorem proving’, in: Bibel, W. and Kowalski, B., Editors,5th CADE, 5th Conference on Automated Deduction, 1980, pp. 264–280.

  12. Plummer, D.,Gazing: A Technique for Controlling the Use of Rewrite Rules. Ph.D. thesis, Department of Artificial Intelligence, University of Edinburgh, May 1988.

  13. Robinson, J. A., ‘A machine-oriented logic based on the resolution principle’,ACM 12, 1965.

  14. SacerdotiE. D., ‘Planning in a hierarchy of abstracton spaces’,Artificial Intelligence 5, 115–135 (1974).

    Article  MATH  Google Scholar 

  15. Sacerdoti, E. D.,A Structure for Plans and Behavior, Artificial Intelligence Series, Elsevier Computer Science Library, 1977.

  16. Siekmann, J., ‘Universal unification’, inProceedings of 7th CADE, Conference on Automated Deduction, 1984.

  17. Sigler, L. E.,Exercises in Set Theory. Van Nostrand Mathematical Studies. Van Nostrand, 1966.

  18. Suppes, S.,Introduction to Logic, The University Series in Undergraduate Mathematics. D. Van Nostrand Company, Inc., 1957.

  19. Wos, L., ‘The problem of definition expansion and contraction’,J. Automated Reasoning 3 (1987).

  20. WosL.,Automated Reasoning: 33 Basic Research Problems. Prentice Hall, Englewood Cliffs, N.J. 1988.

    Google Scholar 

Download references

Author information

Author notes

  1. Dave Barker-Plummer

    Present address: Swarthmore College Computer Science Program, 19081-1397, Swarthmore, PA, USA

Authors and Affiliations

  1. Department of Computer Science, Duke University, 27706, Durham, NC, USA

    Dave Barker-Plummer

Authors
  1. Dave Barker-Plummer
    View author publications

    You can also search for this author in PubMed Google Scholar

Rights and permissions

Reprints and permissions

About this article

Cite this article

Barker-Plummer, D. Gazing: An approach to the problem of definition and lemma use. J Autom Reasoning 8, 311–344 (1992). https://doi.org/10.1007/BF02341853

Download citation

  • Received:

  • Accepted:

  • Issue Date:

  • DOI: https://doi.org/10.1007/BF02341853

Key words

Search

Navigation