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.
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.References
Allen, J. F., ‘Maintaining knowledge about temporal intervals’, Comm. ACM 26, 832–843 (1983).
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).
Andrews, P. B., ‘Theorem proving via general matings’, J. ACM 28, 193–214 (1981).
Bibel, W., Automated Theorem Proving, Friedr. Vieweg & Sohn, Braunschweig, West Germany (1982).
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).
Brachman, R. J., Fikes, R. E., and Levesque, H. J., ‘Krypton: a functional approach to knowledge representation’, IEEE Computer 16, 67–73 (1983).
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).
Brachman, R. J. and Smith, B. C. (eds.), ‘Special issue on knowledge representation’, SIGART Newsletter 70 (1980).
Chang, C. L. and Lee, R. C. T., Symbolic Logic and Mechanical Theorem Proving, Academic Press, New York (1973).
Cohn, A. G., Mechanizing a Particularly Expressive Many Sorted Logic, Ph.D. dissertation, University of Essex, England (1983).
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).
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).
Digricoli, W. J., ‘Resolution by unification and equality’, Proceedings of the Fourth Workshop on Automated Deduction, Austin, Texas, pp. 43–52 (1979).
Dixon, J. K., ‘Z-resolution: theorem-proving with compiled axioms’, J.ACM 20, 127–147 (1973).
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).
Harrison, M. C. and Rubin, N., ‘Another generalization of resolution’, J. ACM 25, 341–351 (1978).
Konolige, D., A Deduction Model of Belief and Its Logics, Ph.D. dissertation, Stanford University, Stanford, California (1984).
Loveland, D. W., Automated Theorem Proving: A Logical Basis, North-Holland, Amsterdam, The Netherlands (1978).
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).
Manna, Z. and Waldinger, R., ‘Special relations in automated deduction’, to appear in J. ACM.
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).
Nelson, G. and Oppen, D. C., ‘Simplification by cooperating decision procedures’, ACM Transactions on Programming Languages and Systems 1, 245–257 (1979).
Nilsson, N. J., Principles of Artificial Intelligence, Tioga Publishing Co., Palo Alto, Calfornia (1980).
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).
Plotkin, G. D., ‘Building-in equational theories’, in Machine Intelligence 7 (eds. Meltzer, B. and Michie, D.) Halsted Press, pp. 73–90 (1972).
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).
Shostak, R. E., ‘Deciding combinations of theories,’ J. ACM 31, 1–12 (1984).
Siekmann, J. H., ‘Universal unification,’ Proceedings of the 7th International Conference on Automated Deduction, Napa, California, pp. 1–42 (1984).
Slagle, J. R. and Norton, L. M., ‘Experiments with an automatic theorem-prover having partial ordering inference rules,’ Comm. ACM 16, 682–688 (1973).
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).
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).
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).
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).
Walther, C., ‘Unification in many-sorted theories,’ Proceedings of the 6th European Conference on Artificial Intelligence, Pisa, Italy (1984).
Wos, L., Overbeek, R., Lusk, E., and Boyle, J., Automated Reasoning, Prentice-Hall, Englewood Cliffs, New Jersey (1984).
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).
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).
Author information
Authors and Affiliations
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
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
Received:
Issue Date:
DOI: https://doi.org/10.1007/BF00244275