• Stan Raatz
Part of the Progress in Computer Science and Applied Logic book series (PCS, volume 10)


Logic Program Univeral Algebra Predicate Logic Horn Clause Automate Theorem Prove 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    Andrews P., Theorem Proving via General Matings, J.ACM 28: 2 (1981), 193–214.CrossRefGoogle Scholar
  2. [2]
    Apt, K.R., Introduction to Logic Programming, TR-87–35, Department of Computer Science, University of Texas at Austin, September 1987. To appear, Handbook of Theoretical Computer Science, van Leeuwen, J., ed., North Holland.Google Scholar
  3. [3]
    Apt, K.R. and van Emden, M.H., Contributions to the Theory of Logic Programming, J.ACM 29: 3 (1982), 841–862.CrossRefGoogle Scholar
  4. [4]
    Chang C.C. and Keisler J.H., Model Theory, North-Holland, Amsterdam, 1978.Google Scholar
  5. [5]
    Chang C.L. and Slagle J.R., Using Rewriting Rules for Connection Graphs to Prove Theorems, Artificial Intelligence 12: 2 (1979), 159–178.CrossRefGoogle Scholar
  6. [6]
    Clark, K.L., Predicate Logic as a Computational Formalism, research report 79/59, Department of Computing, Imperial College.Google Scholar
  7. [7]
    Clark, K.L., Negation as Failure, in Logic and Databases, Galliere and Minker eds, Plenum Press, NY, 293–322.Google Scholar
  8. [8]
    Clark, K.L. and Gregory, S., PARLOG: A Parallel Logic Programming Language, ACM Trans. on Programming Languages and Systems, 8: 1 (1986), 1–49.CrossRefGoogle Scholar
  9. [9]
    Cohn, P.M., Univeral Algebra, D. Reidel Pub. Co., Boston, 1981.Google Scholar
  10. [10]
    Colmerauer, A., Kanoui, H., Roussel, P. and Pasero, R., Un Systeme de Communication Homme-Machine en Francais, Groupe de Recherche en Intelligence Artificielle, Université d’Aix-Marseille, 1972.Google Scholar
  11. [11]
    Connery, J. and Kibler, D., Parallel Interpretation of Logic Programs, Proc. 1981 Conference on Functional Programming Languages and Computer Architecture Vol 1, 163–170Google Scholar
  12. [12]
    Davis, M. and Putnam, H., A Computing Procedure for Quantification Theory, JACM 7 (1960), 201–215.CrossRefGoogle Scholar
  13. [13]
    Dershowitz, N. and Plaisted, D.A., Logic Programming cum Applicative Programming, 1985 IEEE Symposium on Logic Programming,Boston, 54–67.Google Scholar
  14. [14]
    Dowling, W.P. and Gallier, J.H. Linear-time Algorithms for testing the satisfiability of Propositional Horn Formulae, Journal of Logic Programming 1: 3 (1984), 267–284.CrossRefGoogle Scholar
  15. [15]
    Downey, P.J., Sethi, R., and Tarjan, E.R., Variations on the Common Subexpressions Problem. J.ACM 27: 4 (1980), 758–771.CrossRefGoogle Scholar
  16. [16]
    Driscoll, J.R., Sarnak, N., Sleator, D.D., and Tarjan, R.E., Making Data Structures Persistent, 18“ STOC Symposium, Berkeley, CA, 1986, 109–121.Google Scholar
  17. [17]
    van Emden, M. and Kowalski, R.A., The Semantics of Predicate Logic as a Programming Language, J.ACM 23: 4 (1976), 733–742.CrossRefGoogle Scholar
  18. [18]
    Fages, F., Associative-Commutative Unification, Proc. CADE-7, Napa 1984, 194–208.Google Scholar
  19. [19]
    Fages, F. and Huet, G., Unification and Matching in Equational Theories, Proc. CAAP 83, vol. 159, Springer Verlag, l’Aquilla, Italy, 205–220.Google Scholar
  20. [20]
    Fay, M., First-order Unification in an Equational Theory, Proc. 4th Workshop on Automated Deduction, Austin Texas, 1979.Google Scholar
  21. [21]
    Fribourg, L., Oriented Equational Clauses as a Programming Language, J. of Logic Programming 2 (1984), 165–177.CrossRefGoogle Scholar
  22. [22]
    Fribourg, L., SLOG: A Logic Programming Language Interpreter Based on Clausal Superposition and Rewriting, 1985 IEEE Symposium on Logic Programming,Boston, 172–184.Google Scholar
  23. [23]
    Gallaire, H. and Minker, J., (eds.), Logic and Databases, Plenum Press, NY, 1980.Google Scholar
  24. [24]
    Gallier, J.H., Fast Algorithms for Testing Unsatisfiability of Ground Horn Clauses With Equations. Journal of Symbolic Computation 4 (1987), 233254.Google Scholar
  25. [25]
    Gallier, J.H., Logic for Computer Science: Foundations of Automatic Theorem Proving, Harper and Row, 1986.Google Scholar
  26. [26]
    Gallier, J.H. and Raatz, S., Logic Programming and Graph Rewriting, 1985 IEEE Symposium on Logic Programming,Boston, 208–219.Google Scholar
  27. [27]
    Gallier, J.H. and Raatz, S., SLD-Resolution Methods for Horn Clauses with Equality Based on E-Unification, 1986 IEEE Symposium on Logic Programming,Salt Lake City, Utah, 168–179.Google Scholar
  28. [28]
    Gallier, J.Hp. and Raatz, S., HORNLOG: A Graph-based Proof Procedure for Horn clauses, Journal of Logic Programming, 3: 4 (1987), 119–158.CrossRefGoogle Scholar
  29. [29]
    Gallier, J.H. and Raatz, S., Extending SLD-Resolution to Equational Horn Clauses using E-unification, Journal of Logic Programming 5: 1 (1989), 3–47.CrossRefGoogle Scholar
  30. [30]
    Gallier, J.H. and Snyder, W., A General Complete E-unification Procedure, Proceedings of RTA’87, Bordeaux, France, 1987, 114–654.Google Scholar
  31. [31]
    Goguen, J.A., Thatcher, J., Wagner, E., and Wright, J., Initial Algebra Semantics, J.ACM 24 (1977), 68–95.CrossRefGoogle Scholar
  32. [32]
    Goguen, J.A. and Meseguer, J., Eglog: Equality, Types, and Generic Modules for Logic Programming, in: Degroot, D. and Lindstrom, G. (eds.), Functional and Logic Programming, Prentice-Hall, 1985. Short version in J. of Logic Programming 2 (1984), 179–210.Google Scholar
  33. [33]
    Goguen, J.A. and Meseguer, J., Models and Equality for Logical Programming, technical report, SRI International, Menlo Park CA, 1987.Google Scholar
  34. [34]
    Goguen, J.A. and Meseguer, J., Order-Sorted Alegebra Solves the Constructor Selector Problem, LICS, Ithaca, NY, 1987.Google Scholar
  35. [35]
    Green, C., Applications of Theorem Proving to Problem Solving, IJCAI-69, Washington, 1969, 219–239.Google Scholar
  36. [36]
    Hays, P., Computation and Deduction, Proceedings of the Second Symposium on Mathematical Foundations of Computer Science, Czechoslovakia, 1973, 105–118.Google Scholar
  37. [37]
    Herbrand, J. Logical Writings, Reidel, Hingham, MA, 1971.CrossRefGoogle Scholar
  38. [38]
    Hewitt, C., PLANNER: A Language for Proving Theorems in Robots, IJ CAI-69,295–301.Google Scholar
  39. [39]
    Hewitt, C., Procedural Embedding of Knowledge in PLANNER, IJCAI-7, London, 1971.Google Scholar
  40. [40]
    Hill, R., LUSH-Resolution and its Completeness, DCL Memo, Department of Artificial Intelligence, University of Edinburgh, 1974.Google Scholar
  41. [41]
    Hillis, W.D., The Connection Machine. MIT Press, Cambridge, Mass., 1985.Google Scholar
  42. [42]
    Hillis, W.D. and Steele, G.L., Data Parallel Algorithms, CACM, 29: 12 (1986), 1170–1183.CrossRefGoogle Scholar
  43. [43]
    Huet, G., Résolution d’Equations dans les Langages d’Ordre 1, 2,…, w, Thèse d’Etat, Université de Paris V II, 1976.Google Scholar
  44. [44]
    Huet, G. and Hullot, J.M., Proofs by Induction in Equational Theories with Constructors, J. Comp. Sys. Sc., 25 (1982), 239–266.CrossRefGoogle Scholar
  45. [45]
    Huet, G. and Oppen, D. C., Equations and Rewrite Rules: A Survey, in: R. V. Book (ed.), Formal Languages: Perspectives and Open Problems, Academic Press, NY, 1982.Google Scholar
  46. [46]
    Hullot, J.-M., Canonical Forms and Unification, Proc. CADE-5,1980, 318334.Google Scholar
  47. [47]
    Jaffar, J. and Lassez, J.-L., Constraint Logic Programming, techincaI report, IBM Thomas J. Watson Research Center, Yorktown Heights, NY, August 1986.Google Scholar
  48. [48]
    Jaffar, J, Lassez, J.-L, and Lloyd, J.W., Completeness of the Negation as Failure Rule, IJCAI-83,Karlsruhe, 500–506.Google Scholar
  49. [49]
    Jaffar, J., Lassez, J.-L., and Maher, M.J., A Theory of Complete Logic Programs with Equality, J. of Logic Programming 3 (1984), 211–223.Google Scholar
  50. [50]
    Kirchner, C., Méthodes et Outils de Conception Systematique d’Algorithmes d’Unification dans les Theories Equationnelles, Thèse d’Etat, Université de Nancy I, 1985.Google Scholar
  51. [51]
    Kirchner, H., Preuves Par Completion dans les Varietés d’Algèbres, Thèse d’Etat, Université de Nancy I, 1985.Google Scholar
  52. [52]
    Kirchner, C. and Kirchner, H., Contribution à la Resolution d’Equations dans les Algèbres Libres et les Varietés Equationnelles d’Algèbres, Thèse de 3e cycle, Université de Nancy I, 1982.Google Scholar
  53. [53]
    Knuth, D.E. and Bendix, P.B., Simple word problems in univeral algebras, in: Leech, J. (ed.), Computational Problems in Abstract Algebra, Pergamon Press, 1970, 263–297.Google Scholar
  54. [54]
    Kowalski, R.A., Predicate Logic as a Programming Language, IFIP 74, 569574.Google Scholar
  55. [55]
    Kowalski, R.A., Algorithm = Logic + Control, CACM 22: 7 (1979), 424–436.CrossRefGoogle Scholar
  56. [56]
    Kowalski, R.A., A Proof Procedure Using Connection Graphs, J.ACM 22: 4 (1975), 572–595.CrossRefGoogle Scholar
  57. [57]
    Kowalski, R.A. and Kuehner, D., Linear Resolution with Selection Function, Artificial Intelligence 2 (1970), 227–260.CrossRefGoogle Scholar
  58. [58]
    Kozen, D., Complexity of Finitely Presented Algebras, TR 76–294, Department of Computer Science, Cornell University, Ithaca, NY, 1976.Google Scholar
  59. [59]
    Kozen, D., Complexity of Finitely Presented Algebras, 9th STOC Symposium, Boulder Colorado, 1977, 164–177.Google Scholar
  60. [60]
    Kozen, D., Finitely Presented Algebras and the Polynomial Time Hierarchy, TR 77–303, Department of Computer Science, Cornell University, Ithaca, NY, 1977.Google Scholar
  61. [61]
    Lewis, H. and Papadimitriou, C., Elements of the Theory of Computation, Prentice-Hall, Englewood Cliffs, NJ, 1981.Google Scholar
  62. [62]
    LLoyd, J.W., Foundations of Logic Programming, Springer-Verlag, New York, 2nd edition, 1989.Google Scholar
  63. [63]
    Loveland, D.A., Linear Format for Resolution, Proc. IRIA Symposium Automated Demonstration, Versailles, France, 1968, Springer-Verlang, NY, 147162.Google Scholar
  64. [64]
    Loveland, D.A., A Unifying View of Some Linear Herbrand Procedures, JACM 19, 366–384.Google Scholar
  65. [65]
    Loveland, D.A., Automated Theorem Proving: A logical Basis, North Holland, Amsterdam, 1978.Google Scholar
  66. [66]
    Machtey, M. and Young, P.R., An Introduction to the General Theory of Algorithms, Elsevier North-Holland, NY, 1977.Google Scholar
  67. [67]
    Martelli, A. and Montanari, U., An Efficient Unification Algorithm, ACM Toplas 4: 2 (1982), 258–282.CrossRefGoogle Scholar
  68. [68]
    Mota-Oka, T., Fifth Generation Computer Systems, ed., Proc. Int. Conf. on Fifth Generation Computer Systems, JIPDEC, North-Holland, 1982.Google Scholar
  69. [69]
    Nelson G., and Oppen, D.C., Fast Decision Procedures Based on Congruence Closure. J.ACM 27: 2 (1980), 356–364.CrossRefGoogle Scholar
  70. [70]
    Oppen, D.C., Reasoning About Recursively Defined Data Structures, JACM 27: 3 (1980), 403–411.CrossRefGoogle Scholar
  71. [71]
    Paterson, M.S. and Wegman, M.N., Linear Unification, Journal of Computer and Systems Science 16 (1978), 158–167.CrossRefGoogle Scholar
  72. [72]
    Plotkin, G., Building in Equational Theories, in: Machine Intelligence 7 (1972), 73–90.Google Scholar
  73. [73]
    Prawitz, D., An Improved Proof Procedure, Theoria 26 (1960), 102–139.CrossRefGoogle Scholar
  74. [74]
    Raatz, S., Aspects of a Graph-based Proof Procedure for Horn Clauses, Ph.D. thesis, Department of Computer and Information Science, University of Pennsylvania, 1987.Google Scholar
  75. [75]
    Reiter, R. On Closed World Data Bases, in: Gallaire, H. and Minker, J. (eds.), Logic and Databases, Plenum Press, NY, 1980, 55–76.Google Scholar
  76. [76]
    Robinson, J.A., A Machine-oriented Logic Based on the Resolution Principle, JACM 12: 1 (1965), 23–41.CrossRefGoogle Scholar
  77. [77]
    Roussel, P., PROLOG: Manuel de Reference et d’Utilization, Groupe d’Intelligence Artificielle, Université d’Aix-Marseille, 1975.Google Scholar
  78. [78]
    Scott, D.S. and Gunter, C.A., Semantic Domains, draft for chapter in Handbook of Theoretical Computer Science, North Holland, 1987.Google Scholar
  79. [79]
    Sickel, S., Formal Grammars as Models of Logic Derivations, Proc. of IJCAI77, 544–551.Google Scholar
  80. [80]
    Siekmann, J.H., Universal Unification, Proc. CADE-7, Napa, CA, 1984, 1–42.Google Scholar
  81. [81]
    Shapiro, E.Y., A Subset of Concurrent PROLOG and its Interpreter, TR-003, ICOT-Institute for New Generation Computer Technology, Tokyo, Japan, 1983.Google Scholar
  82. [82]
    Slagle, J.R., Automated Theorem Proving for Theories with Simplifiers, Commutativity, and Associativity, J.ACM 21 (1974), 622–642.CrossRefGoogle Scholar
  83. [83]
    Smolka, G., Goguen, J., and Meseguer, J., Order-Sorted Equational Deduction. Techincal report, SRI International, Menlo Park, CA, 1987.Google Scholar
  84. [84]
    Steele, G.D. and Hillis, W.D., Connection Machine LISP: Fined-grained Parallel Symbolic Processing, in 1986 ACM Conference on Lisp and Functional Programming, Cambridge, MA, 279–297.Google Scholar
  85. [85]
    Tiden, E., Symbolic Verification of Switch-Level Circuits using a Prolog Enhanced with Unification in Finite Algebras, Siemens technical report INF2ASE-2–88, 1988.Google Scholar
  86. [86]
    Warren, D., Logic Programming and Compiler Writing, Software Practice and Experience 10 (1980), 97–125.CrossRefGoogle Scholar
  87. [87]
    Warren, D., An Abstract PROLOG Instruction Set, technical note 309, SRI International, Menlo Park, CA, 1983.Google Scholar

Copyright information

© Springer Science+Business Media New York 1990

Authors and Affiliations

  • Stan Raatz
    • 1
  1. 1.Department of Computer ScienceRutgers UniversityNew BrunswickUSA

Personalised recommendations