Springer Nature is making SARS-CoV-2 and COVID-19 research free. View research | View latest news | Sign up for updates

Using hints to increase the effectiveness of an automated reasoning program: Case studies

  • 60 Accesses

  • 30 Citations


In this article we consider the use of hints to help guide the search for a proof. Under the hints strategy, the value of a generated clause is determined, in part, by whether or not the clause subsumes or is subsumed by a user-supplied hint clause. We have implemented the hints strategy and have experimented with it extensively. We summarize our experiences for a variety of reasoning tasks, including proof checking, proof completion, and proof finding. We conclude that the hints strategy has value beyond simply “giving the proof to find the proof.”

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


  1. 1.

    Bledsoe, W. W.: Non-resolution theorem proving, Artificial Intelligence 9 (1977), 1–35.

  2. 2.

    Boyer, R. S., and Moore, J. S. A Computational Logic Handbook, Academic Press, San Diego (1988).

  3. 3.

    Kapur, D. and Zhang, H.: A case study of the completion procedure: Proving ring commutativity problems, in J.-L.Lassez and G.Plotkin (eds), Computational Logic: Essays in Honor of Alan Robinson, MIT Press, Cambridge, MA, 1991, pp. 360–394.

  4. 4.

    Lukasiewicz, J.: Elements of Mathematical Logic, Pergamon Press, Oxford, 1963.

  5. 5.

    Lukasiewicz, J.: Investigations into the sentential calculus, in L.Borkowski (ed.), Jan Lukasiewicz: Selected Works, North-Holland, Amsterdam, 1970, pp. 131–152.

  6. 6.

    McCharen, J., Overbeek, R. A. and Wos, L.: Complexity and related enhancements for automated theorem-proving programs, Computers and Mathematics with Applications 2 (1976), 1–16.

  7. 7.

    McCune, W. W.: OTTER 3.0 Reference Manual and Guide, Technical Report ANL-94/6, Argonne National Laboratory, Argonne, IL, 1994.

  8. 8.

    McCune, W. W.: Private communication, 1994.

  9. 9.

    Smith, B. T.: Reference Manual for the Environmental Theorem Prover, An Incarnation of AURA, Technical Report ANL-88–2, Argonne National Laboratory, Argonne, IL, 1988.

  10. 10.

    Stickel, M. E.: A case study of theorem proving by the Knuth-Bendix method: Discovering that x 3=x implies ring commutativity, in Proc. 7th Conf. on Automated Deduction, Lecture Notes in Computer Science 170, Springer-Verlag, New York, 1984, pp. 248–258.

  11. 11.

    Veroff, R. L.: Canonicalization and Demodulation, Technical Report ANL-81–6, Argonne National Laboratory, Argonne, IL, 1981.

  12. 12.

    Veroff, R. L. and Wos, L.: The linked inference principle, I: The formal treatment, J. Automated Reasoning 8 (1992), 213–274.

  13. 13.

    Veroff, R. L.: An Updated Demodulation Strategy for Ring Problems, Technical Report CS94-12, Department of Computer Science, University of New Mexico, 1994.

  14. 14.

    Wang, T. C.: Case studies of Z-module reasoning: Proving benchmark theorems from ring theory, J. Automated Reasoning 3 (1987), 437–451.

  15. 15.

    Winker, S.: Robbins algebra: conditions that make a near-Boolean algebra Boolean, J. Automated Reasoning 6 (1990), 465–489.

  16. 16.

    Wos, L.: Meeting the challenge of fifty years of logic, J. Automated Reasoning 6 (1990), 213–232.

  17. 17.

    Wos, L.: Automated reasoning and Bledsoe's dream for the field, in R. S.Boyer (ed.), Automated Reasoning: Essays in Honor of Woody Bledsoe, Kluwer Academic Publishers, Dordrecht, 1991, pp. 297–345.

  18. 18.

    Wos, L.: The resonance strategy, Computers and Mathematics with Applications 29 (1995), 133–178.

Download references

Author information

Rights and permissions

Reprints and Permissions

About this article

Cite this article

Veroff, R. Using hints to increase the effectiveness of an automated reasoning program: Case studies. Journal of Automated Reasoning 16, 223–239 (1996).

Download citation

Key words

  • hints strategy
  • automated reasoning programs
  • proof checking
  • proof completion
  • proof finding
  • weighting