Skip to main content
SpringerLink
Log in

Automated deduction by theory resolution

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

Abstract

Theory resolution constitutes a set of complete procedures for incorporating theories into a resolution theorem-proving program, thereby making it unnecessary to resolve directly upon axioms of the theory. This can reduce the length of proofs and the size of the search space. Theory resolution effects a beneficial division of labor, improving the performance of the theorem prover and increasing the applicability of the specialized reasoning procedures. Total theory resolution utilizes a decision procedure that is capable of determining unsatisfiability of any set of clauses using predicates in the theory. Partial theory resolution employs a weaker decision procedure that can determine potential unsatisfiability of sets of literals. Applications include the building in of both mathematical and special decision procedures, e.g., for the taxonomic information furnished by a knowledge representation system. Theory resolution is a generalization of numerous previously known resolution refinements. Its power is demonstrated by comparing solutions of ‘Schubert's Steamroller’ challenge problem with and without building in axioms through theory resolution.

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

Access this article

Log in via an institution

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

References

  1. Allen, J. F., ‘Maintaining knowledge about temporal intervals’, Comm. ACM 26, 832–843 (1983).

    Google Scholar 

  2. Anderson, R. and Bledsoe, W. W., ‘A linear format for resolution with merging and a new technique for establishing completeness’, J. ACM 17, 525–534 (1970).

    Google Scholar 

  3. Andrews, P. B., ‘Theorem proving via general matings’, J. ACM 28, 193–214 (1981).

    Google Scholar 

  4. Bibel, W., Automated Theorem Proving, Friedr. Vieweg & Sohn, Braunschweig, West Germany (1982).

    Google Scholar 

  5. Bledsoe, W. W. and Hines, S. M., ‘Variable elimination and chaining in a resolution-based prover for inequalities’, Proceedings of the 5th Conference on Automated Deduction, Les Arcs, France, 70–87 (1980).

  6. Brachman, R. J., Fikes, R. E., and Levesque, H. J., ‘Krypton: a functional approach to knowledge representation’, IEEE Computer 16, 67–73 (1983).

    Google Scholar 

  7. Brachman, R. J., and Levesque, H. J., ‘Competence in knowledge representation’, Proceedings of the AAAI-82 National Conference on Artificial Intelligence, Pittsburgh, Pennsylvania, 189–192 (1982).

  8. Brachman, R. J. and Smith, B. C. (eds.), ‘Special issue on knowledge representation’, SIGART Newsletter 70 (1980).

  9. Chang, C. L. and Lee, R. C. T., Symbolic Logic and Mechanical Theorem Proving, Academic Press, New York (1973).

    Google Scholar 

  10. Cohn, A. G., Mechanizing a Particularly Expressive Many Sorted Logic, Ph.D. dissertation, University of Essex, England (1983).

    Google Scholar 

  11. Cohn, A. G., ‘Improving the expressiveness of many sorted logic’, Proceedings of the AAAI-83 National conference on Artificial Intelligence, Washington, D.C., pp. 84–87 (1983).

  12. Cohn, A. G., ‘A note concerning the axiomatization of Schubert's steamroller in many sorted logic’, Department of Computer Science, University of Warwick, Coventry, U.K. (1984).

    Google Scholar 

  13. Digricoli, W. J., ‘Resolution by unification and equality’, Proceedings of the Fourth Workshop on Automated Deduction, Austin, Texas, pp. 43–52 (1979).

  14. Dixon, J. K., ‘Z-resolution: theorem-proving with compiled axioms’, J.ACM 20, 127–147 (1973).

    CAS  PubMed  Google Scholar 

  15. Haas, N. and Hendrix, G. G., ‘An approach to acquiring and applying knowledge’, Proceedings of the AAAI-80 National Conference on Artificial Intelligence, Stanford, California, pp. 235–239 (1980).

  16. Harrison, M. C. and Rubin, N., ‘Another generalization of resolution’, J. ACM 25, 341–351 (1978).

    Google Scholar 

  17. Konolige, D., A Deduction Model of Belief and Its Logics, Ph.D. dissertation, Stanford University, Stanford, California (1984).

    Google Scholar 

  18. Loveland, D. W., Automated Theorem Proving: A Logical Basis, North-Holland, Amsterdam, The Netherlands (1978).

    Google Scholar 

  19. Lusk, E. L. and Overbeek, R. A., ‘A portable environment for research in automated reasoning’, Proceedings of the 7th Conference on Automated Deduction, Napa, California, pp. 43–52 (1984).

  20. Manna, Z. and Waldinger, R., ‘Special relations in automated deduction’, to appear in J. ACM.

  21. Morris, J. B., ‘E-resolution: extension of resolution to include the equality relation’, Proceedings of the International Joint Conference on Artificial Intelligence, Washington, D.C., pp. 287–294 (1969).

  22. Nelson, G. and Oppen, D. C., ‘Simplification by cooperating decision procedures’, ACM Transactions on Programming Languages and Systems 1, 245–257 (1979).

    Google Scholar 

  23. Nilsson, N. J., Principles of Artificial Intelligence, Tioga Publishing Co., Palo Alto, Calfornia (1980).

    Google Scholar 

  24. Pigman, V., ‘The interaction between assertional and terminological knowledge in Krypton’, Proceedings of the IEEE Workshop on Principles of Knowledge-Based Systems, Denver, Colorado (1984).

  25. Plotkin, G. D., ‘Building-in equational theories’, in Machine Intelligence 7 (eds. Meltzer, B. and Michie, D.) Halsted Press, pp. 73–90 (1972).

    Google Scholar 

  26. Rich, C., ‘Knowledge representation languages and predicate calculcus: how to have your cake and eat it too,’ Proceedings of the AAAI-82 National Conference on Artificial Intelligence, Pittsburgh, Pennsylvania, pp. 193–196 (1982).

  27. Shostak, R. E., ‘Deciding combinations of theories,’ J. ACM 31, 1–12 (1984).

    Google Scholar 

  28. Siekmann, J. H., ‘Universal unification,’ Proceedings of the 7th International Conference on Automated Deduction, Napa, California, pp. 1–42 (1984).

  29. Slagle, J. R. and Norton, L. M., ‘Experiments with an automatic theorem-prover having partial ordering inference rules,’ Comm. ACM 16, 682–688 (1973).

    Google Scholar 

  30. Stickel, M. E., ‘A nonclausal connection-graph resolution theorem-proving program,’ Proceedings of the AAAI-82 National Conference on Artificial Intelligence, Pittsburgh, Pennsylvania 229–233 (1982).

  31. Stickel, M. E., ‘Theorey resolution: building in nonequational theories,’ Proceedings of the AAAI-83 National Conference on Artificial Intelligence, Washington, D.C., pp. 391–397 (1983).

  32. Walther, C., ‘A many-sorted calculus based on resolution and paramodulation,’ Proceedings of the Eighth International Joint Conference on Artificial Intelligence, Karlsruhe, West Germany, pp. 882–891 (1982).

  33. Walther, C., ‘A mechanical solution of Schubert's steamroller by many-sorted resolution,’ Proceedings of the AAAI-84 National Conference on Artificial Intelligence, Austin, Texas, pp. 330–334 (1984).

  34. Walther, C., ‘Unification in many-sorted theories,’ Proceedings of the 6th European Conference on Artificial Intelligence, Pisa, Italy (1984).

  35. Wos, L., Overbeek, R., Lusk, E., and Boyle, J., Automated Reasoning, Prentice-Hall, Englewood Cliffs, New Jersey (1984).

    Google Scholar 

  36. Wos, L. and Robinson, G. A., ‘Paramodulation and set of support,’ Proceedings of the Symposium on Automatic Demonstration, Versailles, France (1968). In Lecture Notes in Mathematics 125, Springer-Verlag, Berlin, West Germany, pp. 276–310 (1970).

    Google Scholar 

  37. Wos, L., Veroff, R., Smith B., and McCune, W., ‘The linked inference principle, II: the user's viewpoint,’ Proceedings of the 7th International Conference on Automated Deduction, Napa, California, pp. 316–332 (1984).

Download references

Author information

Authors and Affiliations

  1. Artificial Intelligence Center, SRI International, Meulo Park, Calif., USA

    Mark E. Stickel

  2. Center for the Study of Language and Information, Stanford University, Stanford, Calif., USA

    Mark E. Stickel

Authors
  1. Mark E. Stickel
    View author publications

    You can also search for this author in PubMed Google Scholar

Additional information

This research was supported by the Defense Advanced Research Projects Agency under Contract N00039-84-K-0078 with the Naval Electronic Systems Command and was also made possible in part by a gift from the System Development Foundation. The views and conclusions contained in this document are those of the author and should not be interpreted as representative of the official policies, either expressed or implied, of the Defense Advanced Research Projects Agency or the United States government.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Stickel, M.E. Automated deduction by theory resolution. J Autom Reasoning 1, 333–355 (1985). https://doi.org/10.1007/BF00244275

Download citation

  • Received:

  • Issue Date:

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

Key words

Search

Navigation