Advertisement

An introduction to automated deduction

  • Mark E. Stickel
Part Two Knowledge Processing
Part of the Lecture Notes in Computer Science book series (LNCS, volume 232)

Keywords

Unification Algorithm Horn Clause Unit Clause Empty Clause Theory Resolution 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [1]
    Andrews, P.B. Theorem proving via general matings. Journal of the ACM 28, 2 (April 1981), 193–214.CrossRefGoogle Scholar
  2. [2]
    Benanav, D., Kapur, D., and P. Narendran. Complexity of matching problems. Proceedings of the First International Conference on Rewriting Techniques and Applications, Dijon, France, May 1985.Google Scholar
  3. [3]
    Bläsius, K., N. Eisinger, J. Siekmann, G. Smolka, A. Herold, and C. Walther. The Markgraf Karl Refutation Procedure (Fall 1981). Proceedings of the Seventh International Joint Conference on Artificial Intelligence, Vancouver, B.C., Canada, August 1981, 511–518.Google Scholar
  4. [4]
    Bibel, W. On matrices with connections. Journal of the ACM 28, 4 (October 1981), 633–645.CrossRefGoogle Scholar
  5. [5]
    Bibel, W. Automated Theorem Proving. Friedr. Vieweg & Sohn, Braunschweig, West Germany, 1982.Google Scholar
  6. [6]
    Boyer, R.S. and J S. Moore. The sharing of structure in theorem-proving programs. In B. Meltzer and D. Michie (eds.). Machine Intelligence 7. Edinburgh University Press, Edinburgh, Scotland, 1972, pp. 101–116.Google Scholar
  7. [7]
    Brachman, R.J., R.E. Fikes, and H.J. Levesque. Krypton: a functional approach to knowledge representation. IEEE Computer 16, 10 (October 1983), 67–73.Google Scholar
  8. [8]
    Brachman, R.J., V. Pigman Gilbert, and H.J. Levesque. An essential hybrid reasoning system: knowledge and symbol level accounts of Krypton. Proceedings of the Ninth International Joint Conference on Artificial Intelligence, Los Angeles, California, August 1985, 532–539.Google Scholar
  9. [9]
    Brand, D. Proving theorems with the modification method. SIAM Journal of Computing 4 (December 1975), 412–430.CrossRefGoogle Scholar
  10. [10]
    Buchberger, B. Basic features and development of the critical-pair/completion procedure. Proceedings of the First International Conference on Rewriting Techniques and Applications, Dijon, France, May 1985, 1–45.Google Scholar
  11. [11]
    Chang, C.-L. The unit proof and the input proof in theorem proving. Journal of the ACM 17, 4 (October 1970), 698–707.CrossRefGoogle Scholar
  12. [12]
    Chang, C.-L. and R.C.-T. Lee. Symbolic Logic and Mechanical Theorem Proving. Academic Press, New York, New York, 1973.Google Scholar
  13. [13]
    Clocksin, W.F. and C.S. Mellish. Programming in Prolog. Springer-Verlag, Berlin, West Germany, 1981.Google Scholar
  14. [14]
    Cohn, A.G. Mechanizing a Particularly Expressive Many Sorted Logic. Ph.D. dissertation, University of Essex, Essex, England, January 1983.Google Scholar
  15. [15]
    Cohn, A.G. On the solution of Schubert's steamroller in many sorted logic. Proceedings of the Ninth International Joint Conference on Artificial Intelligence, Los Angeles, California, August 1985, 1169–1174.Google Scholar
  16. [16]
    Dahl, V. Translating Spanish into logic through logic. American Journal of Computational Linguistics 7, 3 (September 1981), 149–164.Google Scholar
  17. [17]
    Digricoli, V.J. Resolution by unification and equality. Proceedings of the Fourth Workshop on Automated Deduction, Austin, Texas, February 1979.Google Scholar
  18. [18]
    Digricoli, V.J. The efficacy of RUE resolution: experimental results and heuristic theory. Proceedings of the Seventh International Joint Conference on Artificial Intelligence, Vancouver, B.C., Canada, August 1981, 539–547.Google Scholar
  19. [19]
    Eder, E. Properties of substitutions and unifications. Journal of Symbolic Computation 1 (1985).Google Scholar
  20. [20]
    Fages, F. Associative-commutative unification. Proceedings of the 7th International Conference on Automated Deduction, Napa, California, May 1984. Lecture Notes in Computer Science 170, Springer-Verlag, Berlin, West Germany, pp. 194–208.Google Scholar
  21. [21]
    Fay, M.J. First-order unification in an equational theory. Proceedings of the 4th International Conference on Automated Deduction, Austin, Texas, February 1979, 161–167.Google Scholar
  22. [22]
    Gallier, J. Logic for Computer Science. Harper & Row, New York, New York, 1986.Google Scholar
  23. [23]
    Henschen, L.J. and S.A. Naqvi. An improved filter for literal indexing in resolution systems. Proceedings of the Seventh International Joint Conference on Artificial Intelligence, Vancouver, B.C., Canada, August 1981, 528–529.Google Scholar
  24. [24]
    Hewitt, C. Description and theoretical analysis (using schemata) of PLANNER: a language for proving theorems and manipulating models in a robot. Technical Report, Artificial Intelligence Laboratory, Massachusetts Institute of Technology, Cambridge, Massachusetts, April 1972.Google Scholar
  25. [25]
    Hsiang, J. Refutational theorem proving using term-rewriting systems. Artificial Intelligence Journal 25, 3 (1985), 255–300.CrossRefGoogle Scholar
  26. [26]
    Huet, G. Résolution d'équations dans les langages d'ordre 1,2,...,ω. Thèse d'état, Spècialitè Mathmatiques, Université Paris VII, 1976.Google Scholar
  27. [27]
    Huet, G. An algorithm to generate the basis of solutions to homogeneous diophantine equations. Information Processing Letters 7, 3 (April 1978), 144–147.CrossRefGoogle Scholar
  28. [28]
    Huet, G. Confluent reductions: abstract properties and applications to term rewriting systems. Journal of the ACM 27, 4 (October 1980), 797–821.CrossRefGoogle Scholar
  29. [29]
    Huet, G. A complete proof of correctness of the Knuth-Bendix completion algorithm. Journal of Computer and System Sicences 23 (1981), 11–21.CrossRefGoogle Scholar
  30. [30]
    Huet, G. and D.C. Oppen. Equations and rewrite rules: a survey. Technical Report CSL-111, Computer Science Laboratory, SRI International, Menlo Park, California, January 1980.Google Scholar
  31. [31]
    Hullot, J.-M. A catalogue of canonical term rewriting systems. Technical Report CSL-113, Computer Science Laboratory, SRI International, Menlo Park, California, April 1980.Google Scholar
  32. [32]
    Hullot, J.-M. Canonical forms and unification. Proceedings of the 5th International Conference on Automated Deduction, Les Arcs, France, July 1980. Lecture Notes in Computer Science 87, Springer-Verlag, Berlin, West Germany, pp. 318–334.Google Scholar
  33. [33]
    Jaffar, J., J.-L. Lassez, and J. Lloyd. Completeness of the negation as failure rule. Proceedings of the Eighth International Joint Conference on Artificial Intelligence, Karlsruhe, West Germany, August 1983, 500–506.Google Scholar
  34. [34]
    Jaffar, J. Minimal and complete word unification. Technical Report 51, Department of Computer Science, Monash University, Clayton, Victoria, Australia, March 1985.Google Scholar
  35. [35]
    Jouannaud, J.-P. and H. Kirchner. Completion of a set of rules modulo a set of equations. Technical Note, Computer Science Laboratory, SRI International, Menlo Park, California, April 1984.Google Scholar
  36. [36]
    Knuth, D.E. and P.B. Bendix. Simple word problems in universal algebras. In Leech, J. (ed.), Computational Problems in Abstract Algebras, Pergamon Press, 1970, pp. 263–297.Google Scholar
  37. [37]
    Kowalski, R. A proof procedure using connection graphs. Journal of the ACM 22, 4 (October 1975), 572–595.CrossRefGoogle Scholar
  38. [38]
    Kowalski, R.A. Algorithm=logic+control. Communications of the ACM 22, 7 (July 1979), 424–436.CrossRefGoogle Scholar
  39. [39]
    Kowalski, R. Logic for Problem Solving. Elsevier North-Holland, New York, New York, 1979.Google Scholar
  40. [40]
    Kowalski, R. and D. Kuehner. Linear resolution with selection function. Artificial Intelligence 2 (1971), 227–260.CrossRefGoogle Scholar
  41. [41]
    Lankford, D.S. Canonical algebraic simplification in computational logic. Technical Report, Department of Mathematics, University of Texas, Austin, Texas, May 1975.Google Scholar
  42. [42]
    Lankford, D.S. Canonical inference. Report ATP-32, Department of Mathematics and Computer Sciences, University of Texas at Austin, Austin, Texas, December 1975.Google Scholar
  43. [43]
    Lankford, D.S. and A.M. Ballantyne. Decision procedures for simple equational theories with commutative axioms: Complete sets of commutative reductions. Report ATP-35, Department of Mathematics, University of Texas, Austin, Texas, March 1977.Google Scholar
  44. [44]
    Lankford, D.S. and A.M. Ballantyne. Decision procedures for simple equational theories with permutative axioms: Complete sets of permutative reductions. Report ATP-37, Department of Mathematics, University of Texas, Austin, Texas, April 1977.Google Scholar
  45. [45]
    Lankford, D.S. and A.M. Ballantyne. Decision procedures for simple equational theories with commutative-associative axioms: Complete sets of commutative-associative reductions. Report ATP-39, Department of Mathematics, University of Texas, Austin, Texas, August 1977.Google Scholar
  46. [46]
    Lankford, D., G. Butler, and B. Brady. Abelian group theory unification algorithms for elementary terms. Technical Report, Mathematics Department, Louisiana Tech University, Ruston, Louisiana, 1983.Google Scholar
  47. [47]
    Livesey, M. and J. Siekmann. Termination and decidability results for string unification. Memo CSM-12, Essex University, Essex, England, 1975.Google Scholar
  48. [48]
    Livesey, M. and J. Siekmann. Unification of A+C-terms (bags) and A+C+I-terms (sets). Interner Bericht Nr. 5/76, Institut für Informatik I, Universität Karlsruhe, Karlsruhe, West Germany, 1976.Google Scholar
  49. [49]
    Lloyd, J.W. Foundations of Logic Programming. Springer-Verlag, New York, New York, 1984.Google Scholar
  50. [50]
    Loveland, D.W. A linear format for resolution. Proceedings of the IRIA Symposium on Automatic Demonstration, Versailles, France, 1968. Lecture Notes in Mathematics 125, Springer-Verlag, Berlin, West Germany, 1970, pp. 147–162.Google Scholar
  51. [51]
    Loveland, D.W. A simplified format for the model elimination procedure. Journal of the ACM 16, 3 (July 1969), 349–363.CrossRefGoogle Scholar
  52. [52]
    Loveland, D.W. Automated Theorem Proving: A Logical Basis. North-Holland, Amsterdam, the Netherlands, 1978.Google Scholar
  53. [53]
    Luckham, D. Refinement theorems in resolution theory. Proceedings of the IRIA Symposium on Automatic Demonstration, Verailles, France, 1968. Lecture Notes in Mathematics 125, Springer-Verlag, Berlin, 1970, pp. 163–190.Google Scholar
  54. [54]
    Makanin, G.S. The problem of solvability of equations in a free semigroup. Soviet Akad. Nauk SSSR 233, 2 (1977).Google Scholar
  55. [55]
    Manna, Z. and R. Waldinger. A deductive approach to program synthesis. ACM Transactions on Programming Languages and Systems 2, 1 (January 1980), 90–121.CrossRefGoogle Scholar
  56. [56]
    Manna, Z. and R. Waldinger. The Logical Basis for Computer Programming. Addison-Wesley, Reading, Massachusetts, 1985.Google Scholar
  57. [57]
    Martelli, A. and U. Montanari. An efficient unification algorithm. ACM Transactions on Programming Languages 4, 2 (April 1982), 258–282.CrossRefGoogle Scholar
  58. [58]
    McCharen, J., R. Overbeek, and L. Wos. Complexity and related enhancements for automated theorem-proving programs. Computers and Mathematics with Applications 2 (1976), 1–16.CrossRefGoogle Scholar
  59. [59]
    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., May 1969, 287–294.Google Scholar
  60. [60]
    Murray, N.V. Completely non-clausal theorem proving. Artificial Intelligence 18, 1 (January 1982), 67–85.CrossRefGoogle Scholar
  61. [61]
    Overbeek, R. An implementation of hyperresolution. Computers and Mathematics with Applications 1 (1975), 201–214.CrossRefGoogle Scholar
  62. [62]
    Paterson, M.S. and M.N. Wegman. Linear unification. Journal of Computer and Systems Science 16, 2 (April 1978), 158–167.CrossRefGoogle Scholar
  63. [63]
    Peterson, G.E. and M.E. Stickel. Complete sets of reductions for some equational theories. Journal of the Association for Computing Machinery 28, 2 (April 1981), 233–264.Google Scholar
  64. [64]
    Plaisted, D.A. The occur-check problem in Prolog. New Generation Computing 2, 4 (1984), 309–322.Google Scholar
  65. [65]
    Plotkin, G.D. Building-in equational theories. In Meltzer, B. and D. Michie (eds.). Edinburgh University Press, Edinburgh, Scotland, 1972, pp. 73–90.Google Scholar
  66. [66]
    Robinson, J.A. A machine-oriented logic based on the resolution principle. Journal of the ACM 12, 1 (January 1965), 23–41.CrossRefGoogle Scholar
  67. [67]
    Robinson, J.A. Logic: Form and Function. Elsevier North-Holland, New York, New York, 1979.Google Scholar
  68. [68]
    Rulifson, J.F., J.A. Derksen, and R.J. Waldinger. QA4: a procedural calculus for intuitive reasoning. Technical Note 73, Artificial Intelligence Center, SRI International, Menlo Park, California, November 1972.Google Scholar
  69. [69]
    Schmidt-Schauss, M. A many-sorted calculus with polymorphic functions based on resolution and paramodulation. Proceedings of the Ninth International Joint Conference on Artificial Intelligence, Los Angeles, California, August 1985, 1162–1168.Google Scholar
  70. [70]
    Siekmann, J.H. Unification of commutative terms. Interner Bericht Nr. 2/76, Institut für Informatik I, Universität Karlsruhe, Karlsruhe, West Germany, 1976.Google Scholar
  71. [71]
    Siekmann, J.H. Universal unification. Proceedings of the 7th International Conference on Automated Deduction, Napa, California, May 1984. Lecture Notes in Computer Science 170, Springer-Verlag, Berlin, West Germany, pp. 1–42.Google Scholar
  72. [72]
    Siekmann, J. and W. Stephan. Completeness and soundness of the connection graph proof procedure. Interner Bericht 7/76, Institut für Informatik I, Universität Karlsruhe, Karlsruhe, West Germany, 1976.Google Scholar
  73. [73]
    Slagle, J.R. Automated theorem-proving for theories with simplifiers, commutativity, and associativity. Journal of the ACM 21, 4 (October 1974), 622–642.CrossRefGoogle Scholar
  74. [74]
    Smolka, G. Completeness and confluence properties of Kowalski's clause graph calculus. Interner Bericht 31/82, Institut für Informatik I, Universität Karlsruhe, Karlsruhe, West Germany, December 1982.Google Scholar
  75. [75]
    Stickel, M.E. A complete unification algorithm for associative-commutative functions. Proceedings of the Fifth International Joint Conference on Artificial Intelligence, Tbilisi, Georgia, U.S.S.R., September 1975, 71–76.Google Scholar
  76. [76]
    Stickel, M.E. Mechanical Theorem Proving and Artificial Intelligence Languages. Ph.D. dissertation, Computer Science Department, Carnegic-Mellon University, Pittsburgh, Pennsylvania, December 1977.Google Scholar
  77. [77]
    Stickel, M.E. A unification algorithm for associative-commutative functions. Journal of the ACM 28, 3 (July 1981), 423–434.CrossRefGoogle Scholar
  78. [78]
    Stickel, M.E. A nonclausal connection-graph resolution theorem-proving program. Proceedings of the AAAI-82 National Conference on Artificial Intelligence, Pittsburgh, Pennsylvania, August 1982, 229–233.Google Scholar
  79. [79]
    Stickel, M.E. Theory resolution: building in nonequational theories. Proceedings of the AAAI-83 National Conference on Artificial Intelligence, Washington, D.C., August 1983, 391–397.Google Scholar
  80. [80]
    Stickel, M.E. A Prolog technology theorem prover. New Generation Computing 2, 4 (1984), 371–383.Google Scholar
  81. [81]
    Stickel, M.E. Automated deduction by theory resolution. Journal of Automated Reasoning 1, 4 (1985), 333–355.CrossRefGoogle Scholar
  82. [82]
    Stickel, M.E. and W.M. Tyson. An analysis of consecutively bounded depth-first search with applications in automated deduction. Proceedings of the Ninth International Joint Conference on Artificial Intelligence, Los Angeles, California, August 1985, 1073–1075.Google Scholar
  83. [83]
    van Vaalen, J. An extension of unification to substitutions with an application to automatic theorem proving. Proceedings of the Fifth International Joint Conference on Artificial Intelligence, Tbilisi, Georgia, U.S.S.R., September 1975, 77–82.Google Scholar
  84. [84]
    Walther, C. A many-sorted calculus based on resolution and paramodulation. Proceedings of the Eighth International Joint Conference on Artificial Intelligence, Karlsruhe, West Germany, August 1983, 882–891.Google Scholar
  85. [85]
    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, August 1984, 330–334. Revised version appeared in Artificial Intelligence 26, 2 (May 1985), 217–224.CrossRefGoogle Scholar
  86. [86]
    Walther, C. Unification in many-sorted theories. Proceedings of the 6th European Conference on Artificial Intelligence, Pisa, Italy, September 1984.Google Scholar
  87. [87]
    Winker, S.K. and L. Wos. Procedure implementation through demodulation and related tricks. Proceedings of the 6th International Conference on Automated Deduction, New York, New York, June 1982. Lecture Notes in Computer Science 138, Springer-Verlag, Berlin, West Germany, pp. 109–131.Google Scholar
  88. [88]
    Wos, L., R. Overbeek, E. Lusk, and J. Boyle. Automated Reasoning. Prentice-Hall, Englewood Cliffs, New Jersey, 1984.Google Scholar
  89. [89]
    Wos, L. and G.A. Robinson Paramodulation and set of support. Proceedings of the IRIA Symposium on Automatic Demonstration, Verailles, France, 1968. Lecture Notes in Mathematics 125, Springer-Verlag, Berlin, 1970, pp. 276–310.Google Scholar
  90. [90]
    Wos, L., G.A. Robinson, and D.F. Carson. Efficiency and completeness of the set of support strategy in theorem proving. Journal of the ACM 12, 4 (October 1965), 536–541.CrossRefGoogle Scholar
  91. [91]
    Wos, L., G.A. Robinson, D.F. Carson, and L. Shalla. The concept of demodulation in theorem proving. Journal of the ACM 14, 4 (October 1967), 698–709.CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1986

Authors and Affiliations

  • Mark E. Stickel
    • 1
  1. 1.Artificial Intelligence Center SRI InternationalMenlo Park

Personalised recommendations