Skip to main content
SpringerLink
Log in
Book cover

Programming Logics pp 1–18Cite as

Harald Ganzinger’s Legacy: Contributions to Logics and Programming

  • Chapter

  • 1051 Accesses

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 7797))

Abstract

In 2004 Harald Ganzinger was nominated for the Herbrand Award, which he received only two months before he passed away on June 3, 2004. We describe Ganzinger’s scientific achievements. We hope that this paper will also be useful as a reference guide to Ganzinger’s most significant contributions and publications in many areas of computer science.

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

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Armando, A., Bonacina, M.P., Ranise, S., Schulz, S.: New results on rewrite-based satisfiability procedures. ACM Transactions on Computational Logic 10(1), 1–47 (2009)

    Article  MathSciNet  Google Scholar 

  2. Althaus, E., Kruglov, E., Weidenbach, C.: Superposition Modulo Linear Arithmetic SUP(LA). In: Ghilardi, S., Sebastiani, R. (eds.) FroCoS 2009. LNCS, vol. 5749, pp. 84–99. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  3. Armando, A., Ranise, S., Rusinowitch, M.: A rewriting approach to satisfiability procedures. Information and Computation 183(2), 140–164 (2003)

    Article  MathSciNet  MATH  Google Scholar 

  4. Bachmair, L., Dershowitz, N.: Critical pair criteria for completion. Journal of Symbolic Computation 6(1), 1–18 (1988)

    Article  MathSciNet  MATH  Google Scholar 

  5. Bertling, H., Ganzinger, H.: Completion-time optimization of rewrite-time goal solving. In: Extended Abstracts of the Third International Workshop on Unification (Preliminary Version) (1989)

    Google Scholar 

  6. Bachmair, L., Ganzinger, H.: Completion of first-order clauses with equality by strict superposition (abstract). In: Term Rewriting: Theory and Applications (Ext. Abstracts of the 2nd German Workshop) (1990)

    Google Scholar 

  7. Bachmair, L., Ganzinger, H.: Completion of First-order Clauses with Equality by Strict Superposition (Extended Abstract). In: Okada, M., Kaplan, S. (eds.) CTRS 1990. LNCS, vol. 516, pp. 162–180. Springer, Heidelberg (1991)

    Chapter  Google Scholar 

  8. Bachmair, L., Ganzinger, H.: On Restrictions of Ordered Paramodulation with Simplification. In: Stickel, M.E. (ed.) CADE 1990. LNCS (LNAI), vol. 449, pp. 427–441. Springer, Heidelberg (1990)

    Chapter  Google Scholar 

  9. Bachmair, L., Ganzinger, H.: Perfect model semantics for logic programs with equality. In: Furukawa, K. (ed.) Proceedings of the Eighth International Conference on Logic Programming, Paris, France, June 24-28, pp. 645–659. The MIT Press (1991)

    Google Scholar 

  10. Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification. Technical Report MPI-I-91-208, Max-Planck-Institut für Informatik, Saarbrücken (August 1991)

    Google Scholar 

  11. Bachmair, L., Ganzinger, H.: Non-clausal Resolution and Superposition with Selection and Redundancy Criteria. In: Voronkov, A. (ed.) LPAR 1992. LNCS, vol. 624, pp. 273–284. Springer, Heidelberg (1992)

    Chapter  Google Scholar 

  12. Bachmair, L., Ganzinger, H.: Associative-commutative superposition. Technical Report MPI-I-93-267, Max-Planck-Institut für Informatik, Saarbrücken (December 1993)

    Google Scholar 

  13. Bachmair, L., Ganzinger, H.: Associative-commutative Superposition. In: Lindenstrauss, N., Dershowitz, N. (eds.) CTRS 1994. LNCS, vol. 968, pp. 155–167. Springer, Heidelberg (1995)

    Chapter  Google Scholar 

  14. Bachmair, L., Ganzinger, H.: Buchberger’s Algorithm: A Constraint-based Completion Procedure. In: Jouannaud, J.-P. (ed.) CCL 1994. LNCS, vol. 845, pp. 285–301. Springer, Heidelberg (1994)

    Chapter  Google Scholar 

  15. Bachmair, L., Ganzinger, H.: Ordered Chaining for Total Orderings. In: Bundy, A. (ed.) CADE 1994. LNCS (LNAI), vol. 814, pp. 435–450. Springer, Heidelberg (1994)

    Chapter  Google Scholar 

  16. Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification. Journal of Logic and Computation 4(3), 217–247 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  17. Bachmair, L., Ganzinger, H.: Rewrite techniques for transitive relations. In: Ninth Annual IEEE Symposium on Logic in Computer Science, Paris, France (July 1994)

    Google Scholar 

  18. Basin, D., Ganzinger, H.: Complexity Analysis Based on Ordered Resolution. In: Eleventh Annual IEEE Symposium on Logic in Computer Science (LICS). IEEE Computer Society Press, New Brunswick, New Jersey, USA, pp. 456–465. IEEE Computer Society Press (1996)

    Google Scholar 

  19. Bachmair, L., Ganzinger, H.: Ordered chaining calculi for first-order theories of transitive relations. Journal of the ACM 45(6) (November 1998); Revised Version of MPI-I-95-2-00

    Google Scholar 

  20. Bachmair, L., Ganzinger, H.: Equational reasoning in saturation-based theorem proving. In: Bibel, W., Schmitt, P. (eds.) Automated Deduction: A Basis for Applications. Kluwer (1998)

    Google Scholar 

  21. Bachmair, L., Ganzinger, H.: Strict Basic Superposition. In: Kirchner, C., Kirchner, H. (eds.) CADE 1998. LNCS (LNAI), vol. 1421, pp. 160–174. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  22. Bachmair, L., Ganzinger, H.: Resolution theorem proving. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. I, ch. 2, pp. 19–99. Elsevier (2001)

    Google Scholar 

  23. Basin, D.A., Ganzinger, H.: Automated complexity analysis based on ordered resolution. Journal of the ACM 48(1), 70–109 (2001)

    Article  MathSciNet  MATH  Google Scholar 

  24. Bertling, H., Ganzinger, H., Baumeister, H.: CEC (Conditional Equations Completion). In: Brandenburg, F.J., Vidal-Naquet, G., Wirsing, M. (eds.) STACS 1987. LNCS, vol. 247, p. 470. Springer, Heidelberg (1987)

    Google Scholar 

  25. Bachmair, L., Ganzinger, H., Lynch, C., Snyder, W.: Basic Paramodulation and Superposition. In: Kapur, D. (ed.) CADE 1992. LNCS (LNAI), vol. 607, pp. 462–476. Springer, Heidelberg (1992)

    Google Scholar 

  26. Bachmair, L., Ganzinger, H., Lynch, C., Snyder, W.: Basic paramodulation. Information and Computation 121(2), 172–192 (1995)

    Article  MathSciNet  MATH  Google Scholar 

  27. Bofill, M., Godoy, G., Nieuwenhuis, R., Rubio, A.: Paramodulation with non-monotonic orderings. In: 14th IEEE Symposium on Logic in Computer Science (LICS), Trento, Italy, July 2-5, vol. 5, pp. 225–233 (1999)

    Google Scholar 

  28. Bertling, H., Ganzinger, H., Schäfers, R.: CEC: A system for conditional equational completion — User manual, version 1.0 (1988)

    Google Scholar 

  29. Bertling, H., Ganzinger, H., Schäfers, R.: CEC: A system for the completion of conditional equational specifications. In: Ganzinger, H. (ed.) ESOP 1988. LNCS, vol. 300, pp. 378–379. Springer, Heidelberg (1988)

    Chapter  Google Scholar 

  30. Bertling, H., Ganzinger, H., Schäfers, R.: A collection of specifications completed by the CEC-system, version 1.0 (1988)

    Google Scholar 

  31. Bachmair, L., Ganzinger, H., Stuber, J.: Combining Algebra and Universal Algebra in First-order Theorem Proving: The Case of Commutative Rings. In: Reggio, G., Astesiano, E., Tarlecki, A. (eds.) Abstract Data Types 1994 and COMPASS 1994. LNCS, vol. 906, pp. 1–29. Springer, Heidelberg (1995)

    Chapter  Google Scholar 

  32. Bachmair, L., Ganzinger, H., Voronkov, A.: Elimination of Equality via Transformation with Ordering Constraints. In: Kirchner, C., Kirchner, H. (eds.) CADE 1998. LNCS (LNAI), vol. 1421, pp. 175–190. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  33. Bachmair, L., Ganzinger, H., Waldmann, U.: Theorem Proving for Hierarchic First-order Theories. In: Kirchner, H., Levi, G. (eds.) ALP 1992. LNCS, vol. 632, pp. 420–434. Springer, Heidelberg (1992)

    Chapter  Google Scholar 

  34. Bachmair, L., Ganzinger, H., Waldmann, U.: Set constraints are the monadic class. In: Eighth Annual IEEE Symposium on Logic in Computer Science (LICS), Montreal, Canada, pp. 75–83. IEEE Computer Society Press (1993)

    Google Scholar 

  35. Bachmair, L., Ganzinger, H., Waldmann, U.: Superposition with Simplification as a Decision Procedure for the Monadic Class with Equality. In: Mundici, D., Gottlob, G., Leitsch, A. (eds.) KGC 1993. LNCS, vol. 713, pp. 83–96. Springer, Heidelberg (1993)

    Chapter  Google Scholar 

  36. Bachmair, L., Ganzinger, H., Waldmann, U.: Refutational theorem proving for hierarchic first-order theories. Appl. Algebra Eng. Commun. Comput. 5, 193–212 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  37. Comon, H., Nieuwenhuis, R.: Induction = I-Axiomatization + First-Order Consistency. Information & Computation 159(1), 151–186 (2000)

    Article  MathSciNet  MATH  Google Scholar 

  38. Degtyarev, A., Fisher, M., Konev, B.: Monodic temporal resolution. ACM Trans. Comput. Log. 7(1), 108–150 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  39. Eggers, A., Kruglov, E., Kupferschmid, S., Scheibler, K., Teige, T., Weidenbach, C.: Superposition Modulo Non-linear Arithmetic. In: Tinelli, C., Sofronie-Stokkermans, V. (eds.) FroCoS 2011. LNCS, vol. 6989, pp. 119–134. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  40. Ganzinger, H.: Darstellung der Artanpassung in höheren Programmiersprachen durch Repräsentation von Gruppen. In: Schneider, H.J., Nagl, M. (eds.) Programmiersprachen, 4. Fachtagung der GI, Erlangen, Proceedings, März 8-10. Informatik-Fachberichte, vol. 1, pp. 194–202. Springer (1976)

    Google Scholar 

  41. Ganzinger, H.: An approach to the derivation of compiler description concepts from the mathematical semantics concept. In: Böhling, K.-H., Spies, P.P. (eds.) GI - 9. Jahrestagung, Bonn, Proceedings, Oktober 1-5. Informatik-Fachberichte, vol. 19, pp. 206–217. Springer (1979)

    Google Scholar 

  42. Ganzinger, H.: On Storage Optimization for Automatically Generated Compilers. In: Weihrauch, K. (ed.) GI-TCS 1979. LNCS, vol. 67, pp. 132–141. Springer, Heidelberg (1979)

    Google Scholar 

  43. Ganzinger, H.: Transforming denotational semantics into practical attribute grammars. In: Jones, N.D. (ed.) Semantics-Directed Compiler Generation. LNCS, vol. 94, pp. 1–69. Springer, Heidelberg (1980)

    Chapter  Google Scholar 

  44. Ganzinger, H.: Description of parameterized compiler modules. In: Brauer, W. (ed.) GI - 11. Jahrestagung in Verbindung mit Third Conference of the European Co-operation in Informatics (ECI), München, Proceedings, Oktober 20.-23. Informatik-Fachberichte, vol. 50, pp. 11–19. Springer (1981)

    Google Scholar 

  45. Ganzinger, H.: Increasing modularity and language-independency in automatically generated compilers. Sci. Comput. Program. 3(3), 223–278 (1983)

    Article  MathSciNet  MATH  Google Scholar 

  46. Ganzinger, H.: Modular compiler descriptions based on abstract semantic data types. In: Proceedings 2nd Workshop on Abstract Data Types, University of Passau (1983)

    Google Scholar 

  47. Ganzinger, H.: Modular Compiler Descriptions Based on Abstract Semantic Data Types (Extended Abstract). In: Díaz, J. (ed.) ICALP 1983. LNCS, vol. 154, pp. 237–249. Springer, Heidelberg (1983)

    Chapter  Google Scholar 

  48. Ganzinger, H.: Parameterized specifications: Parameter passing and implementation with respect to observability. ACM Transactions on Programming Languages and Systems 5(3), 318–354 (1983)

    Article  MathSciNet  MATH  Google Scholar 

  49. Ganzinger, H.: Knuth-Bendix completion for parametric specifications with conditional equations. In: Workshop on Specification of Abstract Data Types, ADT (1986)

    Google Scholar 

  50. Ganzinger, H.: A completion procedure for conditional equations. In: Kaplan, S., Jouannaud, J.-P. (eds.) CTRS 1987. LNCS, vol. 308, pp. 62–83. Springer, Heidelberg (1988)

    Chapter  Google Scholar 

  51. Ganzinger, H.: Completion with History-dependent Complexities for Generated Equations. In: Sannella, D., Tarlecki, A. (eds.) Abstract Data Types 1987. LNCS, vol. 332, pp. 73–91. Springer, Heidelberg (1988)

    Chapter  Google Scholar 

  52. Ganzinger, H.: Ground Term Confluence in Parametric Conditional Equational Specifications. In: Brandenburg, F.J., Wirsing, M., Vidal-Naquet, G. (eds.) STACS 1987. LNCS, vol. 247, pp. 286–298. Springer, Heidelberg (1987)

    Chapter  Google Scholar 

  53. Ganzinger, H.: Order-sorted Completion: The Many-sorted Way (Extended Abstract). In: Díaz, J., Yu, Y. (eds.) CAAP 1989 and TAPSOFT 1989. LNCS, vol. 351, pp. 244–258. Springer, Heidelberg (1989)

    Google Scholar 

  54. Ganzinger, H.: A Completion Procedure for Conditional Equations. Journal of Symbolic Computation 11, 51–81 (1991)

    Article  MathSciNet  MATH  Google Scholar 

  55. Ganzinger, H.: Order-sorted completion: the many-sorted way. Theoretical Computer Science 89, 3–32 (1991)

    Article  MathSciNet  MATH  Google Scholar 

  56. Ganzinger, H.: Shostak Light. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 332–346. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  57. Ganzinger, H., de Nivelle, H.: A superposition decision procedure for the guarded fragment with equality. In: 14th IEEE Symposium on Logic in Computer Science (LICS), Trento, Italy, July 2–5, pp. 295–305 (1999)

    Google Scholar 

  58. Ganzinger, H., Giegerich, R., Möncke, U., Wilhelm, R.: A truly generative semantics-directed compiler generator. In: SIGPLAN Symposium on Compiler Construction, pp. 172–184 (1982)

    Google Scholar 

  59. Ganzinger, H., Heeg, G., Baumeister, H., Rüger, M.: Smalltalk-80. Informationstechnik — IT 29(4), 241–251 (1987)

    Google Scholar 

  60. Ganzinger, H., Hustadt, U., Meyer, C., Schmidt, R.A.: A resolution-based decision procedure for extensions of K4. In: Zakharyaschev, M., Segerberg, K., de Rijke, M., Wansing, H. (eds.) Advances in Modal Logic 2, Papers from the Second Workshop on Advances in Modal Logic, Uppsala, Sweden, pp. 225–246. CSLI Publications (1998)

    Google Scholar 

  61. Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: DPLL(T): Fast Decision Procedures. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 175–188. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  62. Ganzinger, H., Hillenbrand, T., Waldmann, U.: Superposition Modulo a Shostak Theory. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol. 2741, pp. 182–196. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  63. Ganzinger, H., Jacquemard, F., Veanes, M.: Rigid reachability, the non-symmetric form of rigid E-unification. Int. J. Found. Comput. Sci. 11(1), 3–27 (2000)

    Article  MathSciNet  MATH  Google Scholar 

  64. Ganzinger, H., Korovin, K.: New directions in instantiation-based theorem proving. In: Proc.18th IEEE Symposium on Logic in Computer Science (LICS 2003), pp. 55–64. IEEE Computer Society Press (2003)

    Google Scholar 

  65. Ganzinger, H., Korovin, K.: Integrating equational reasoning into instantiation-based theorem proving. In: Marcinkowski, J., Tarlecki, A. (eds.) CSL 2004. LNCS, vol. 3210, pp. 71–84. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  66. Ganzinger, H., Korovin, K.: Theory Instantiation. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol. 4246, pp. 497–511. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  67. Ganzinger, H., Meyer, C., Veanes, M.: The two-variable guarded fragment with transitive relations. In: 14th IEEE Symposium on Logic in Computer Science (LICS), Trento, Italy, July 2-5, pp. 24–34 (1999)

    Google Scholar 

  68. Ganzinger, H., Meyer, C., Weidenbach, C.: Soft Typing for Ordered Resolution. In: McCune, W. (ed.) CADE 1997. LNCS (LNAI), vol. 1249, pp. 321–335. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  69. Godoy, G., Nieuwenhuis, R.: Paramodulation with built-in abelian groups. In: 15th IEEE Symp. Logic in Computer Science (LICS), Santa Barbara, USA, pp. 413–424. IEEE Computer Society Press (2000)

    Google Scholar 

  70. Ganzinger, H., Nieuwenhuis, R.: Constraints and Theorem Proving. In: Comon, H., Marché, C., Treinen, R. (eds.) CCL 1999. LNCS, vol. 2002, pp. 159–201. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  71. Godoy, G., Nieuwenhuis, R.: Ordering Constraints for Deduction with Built-in Abelian Semigroups, Monoids and Groups. In: 16th IEEE Symposium on Logic in Computer Science (LICS), Boston, USA, June 16–20, pp. 38–47. IEEE Computer Society Press (2001)

    Google Scholar 

  72. Godoy, G., Nieuwenhuis, R.: Superposition with Completely Built-in Abelian Groups. Journ. Symbolic Computation 37(1), 1–33 (2004)

    Article  MathSciNet  MATH  Google Scholar 

  73. Ganzinger, H., Nieuwenhuis, R., Nivela, P.: The Saturate System (1999), Software and documentation, http://www.mpi-inf.mpg.de/SATURATE/Saturate.html

  74. Ganzinger, H., Nieuwenhuis, R., Nivela, P.: Context trees. In: EuroGP 2001. LNCS (LNAI), vol. 2038, pp. 242–256, Siena, Italy (2001)

    Google Scholar 

  75. Ganzinger, H., Nieuwenhuis, R., Nivela, P.: Fast term indexing with coded context trees. Journal of Automated Reasoning 32(2), 103–120 (2004)

    Article  MathSciNet  MATH  Google Scholar 

  76. Graf, P.: Substitution Tree Indexing. In: Hsiang, J. (ed.) RTA 1995. LNCS, vol. 914, pp. 117–131. Springer, Heidelberg (1995)

    Chapter  Google Scholar 

  77. Ganzinger, H., Ripken, K., Wilhelm, R.: Automatic generation of optimizing multipass compilers. In: IFIP Congress, pp. 535–540 (1977)

    Google Scholar 

  78. Ganzinger, H., Stuber, J.: Inductive Theorem Proving by Consistency for First-order Clauses. In: Rusinowitch, M., Remy, J.-L. (eds.) CTRS 1992. LNCS, vol. 656, pp. 226–241. Springer, Heidelberg (1993)

    Chapter  Google Scholar 

  79. Ganzinger, H., Stuber, J.: Superposition with equivalence reasoning and delayed clause normal form transformation. Inf. Comput. 199(1-2), 3–23 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  80. Ganzinger, H., Sofronie-Stokkermans, V.: Chaining techniques for automated theorem proving in many-valued logics. In: 30th IEEE International Symposium on Multiple-Valued Logic (ISMV)L, pp. 337–344 (2000)

    Google Scholar 

  81. Ganzinger, H., Sofronie-Stokkermans, V., Waldmann, U.: Modular proof systems for partial functions with Evans equality. Inf. Comput. 204(10), 1453–1492 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  82. Ganzinger, H., Wilhelm, R.: Verschränkung von Compiler-Moduln. In: Mühlbacher, J.R. (ed.) GI 1975. LNCS, vol. 34, pp. 654–665. Springer, Heidelberg (1975)

    Chapter  Google Scholar 

  83. Ganzinger, H., Waldmann, U.: Termination Proofs of Well-moded Logic Programs via Conditional Rewrite Systems. In: Rusinowitch, M., Remy, J.-L. (eds.) CTRS 1992. LNCS, vol. 656, pp. 430–437. Springer, Heidelberg (1993)

    Chapter  Google Scholar 

  84. Ganzinger, H., Waldmann, U.: Theorem Proving in Cancellative Abelian Monoids. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS (LNAI), vol. 1104, pp. 388–402. Springer, Heidelberg (1996)

    Chapter  Google Scholar 

  85. Herbrand, J.: Recherches sur la théorie de la démonstration. Traveaux de la Societé des Sciences de Varsoria 33 (1930); Translation appeared in van Heijenoort, J.: From Frege to Gödel: A Source Book in Mathematical Logic, pp. 525–581. Harvard University Press (1967)

    Google Scholar 

  86. Hillenbrand, T.: Superposition and Decision Procedures – Back and Forth. PhD thesis, Universität des Saarlandes (2008)

    Google Scholar 

  87. Hoder, K., Kovács, L., Voronkov, A.: Interpolation and Symbol Elimination in Vampire. In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS, vol. 6173, pp. 188–195. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  88. Hustadt, U., Motik, B., Sattler, U.: Deciding expressive description logics in the framework of resolution. Inf. Comput. 206(5), 579–601 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  89. Hillenbrand, T., Weidenbach, C.: Superposition for finite domains. Research Report MPI-I-2007-RG1-002, Max-Planck Institute for Informatics, Saarbruecken, Germany (April 2007)

    Google Scholar 

  90. Horbach, M., Weidenbach, C.: Superposition for fixed domains. ACM Transactions on Computational Logic 11(4), 1–35 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  91. Jacquemard, F., Meyer, C., Weidenbach, C.: Unification in Extensions of Shallow Equational Theories. In: Nipkow, T. (ed.) RTA 1998. LNCS, vol. 1379, pp. 76–90. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  92. Jacquemard, F., Rusinowitch, M., Vigneron, L.: Tree Automata with Equality Constraints Modulo Equational Theories. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 557–571. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  93. Knuth, D.E., Bendix, P.B.: Simple word problems in universal algebras. In: Leech, I. (ed.) Computational Problems in Abstract Algebra, pp. 263–297. Pergamon Press (1970)

    Google Scholar 

  94. Kirchner, C., Kirchner, H., Rusinowitch, M.: Deduction with symbolic constraints. Revue Française d’Intelligence Artificielle 4(3), 9–52 (1990)

    Google Scholar 

  95. Kazakov, Y., Motik, B.: A resolution-based decision procedure for shoiq. Journal of Automated Reasoning 40(2-3), 89–116 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  96. Kapur, D., Musser, D.R., Narendran, P.: Only prime superpositions need be considered in the Knuth-Bendix completion procedure. Journal of Symbolic Computation 6(1), 19–36 (1988)

    Article  MathSciNet  MATH  Google Scholar 

  97. Korovin, K., Voronkov, A.: Integrating Linear Arithmetic into Superposition Calculus. In: Duparc, J., Henzinger, T.A. (eds.) CSL 2007. LNCS, vol. 4646, pp. 223–237. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  98. Lev-Ami, T., Weidenbach, C., Reps, T.W., Sagiv, M.: Labelled Clauses. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 311–327. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  99. Lynch, C., Snyder, W.: Redundancy criteria for constrained completion. Theoretical Compututer Science 142(2), 141–177 (1995)

    Article  MathSciNet  MATH  Google Scholar 

  100. Levy, J., Veanes, M.: On the undecidability of second-order unification. Inf. Comput. 159(1-2), 125–150 (2000)

    Article  MathSciNet  MATH  Google Scholar 

  101. McAllester, D.: Automatic recognition of tractability in inferences relations. Journal of the ACM 40(2), 284–303 (1993)

    Article  MathSciNet  MATH  Google Scholar 

  102. McCune, W.: Solution of the Robbins problem. Journal of Automated Reasoning 19(3), 263–276 (1997)

    Article  MathSciNet  MATH  Google Scholar 

  103. McMillan, K.L.: Interpolation and SAT-based Model Checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 1–13. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  104. Nieuwenhuis, R.: Basic paramodulation and decidable theories. In: Eleventh Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, USA, pp. 473–482. IEEE Computer Society Press (1996)

    Google Scholar 

  105. Nipkow, T.: More Church-Rosser Proofs (in Isabelle/HOL). In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol. 1104, pp. 733–747. Springer, Heidelberg (1996)

    Chapter  Google Scholar 

  106. Nivela, P., Nieuwenhuis, R.: Practical Results on the Saturation of Full First-order Clauses: Experiments with the Saturate System (System Description). In: Kirchner, C. (ed.) RTA 1993. LNCS, vol. 690, pp. 436–440. Springer, Heidelberg (1993)

    Chapter  Google Scholar 

  107. Nieuwenhuis, R., Rubio, A.: Basic Superposition is Complete. In: Krieg-Brückner, B. (ed.) ESOP 1992. LNCS, vol. 582, pp. 371–390. Springer, Heidelberg (1992)

    Chapter  Google Scholar 

  108. Nieuwenhuis, R., Rubio, A.: Theorem Proving with Ordering Constrained Clauses. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 477–491. Springer, Heidelberg (1992)

    Google Scholar 

  109. Nieuwenhuis, R., Rubio, A.: AC-Superposition with Constraints: No AC-unifiers Needed. In: Bundy, A. (ed.) CADE 1994. LNCS, vol. 814, pp. 545–559. Springer, Heidelberg (1994)

    Chapter  Google Scholar 

  110. Nieuwenhuis, R., Rubio, A.: Theorem Proving with Ordering and Equality Constrained Clauses. Journal of Symbolic Computation 19(4), 321–351 (1995)

    Article  MathSciNet  MATH  Google Scholar 

  111. Peterson, G.E.: A technique for establishing completeness results in theorem proving with equality. SIAM J. on Computing 12(1), 82–100 (1983)

    Article  MathSciNet  MATH  Google Scholar 

  112. Robinson, J.A.: A machine-oriented logic based on the resolution principle. Journal of the ACM 12(1), 23–41 (1965)

    Article  MathSciNet  MATH  Google Scholar 

  113. Riazanov, A., Voronkov, A.: The design and implementation of VAMPIRE. AI Communications 15(91-110) (2002)

    Google Scholar 

  114. Robinson, G.A., Wos, L.T.: Paramodulation and theorem-proving in first order theories with equality. Machine Intelligence 4, 135–150 (1969)

    MathSciNet  MATH  Google Scholar 

  115. Schulz, S., Bonacina, M.P.: On handling distinct objects in the superposition calculus. In: Notes 5th IWIL Workshop on the Implementation of Logics, pp. 11–66 (2005)

    Google Scholar 

  116. Stephan Schulz, E.: A Brainiac Theorem Prover. Journal of AI Communications 15(2/3), 111–126 (2002)

    MATH  Google Scholar 

  117. Schmidt, R.A., Hustadt, U.: A Resolution Decision Procedure for Fluted Logic. In: McAllester, D. (ed.) CADE 2000. LNCS, vol. 1831, pp. 433–448. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  118. Schmidt, R.A., Hustadt, U.: The axiomatic translation principle for modal logic. ACM Trans. Comput. Log. 8(4), 1–51 (2007)

    Article  MathSciNet  Google Scholar 

  119. Seidl, H., Reuß, A.: Extending \({\cal H}_1\)-Clauses with Path Disequalities. In: Birkedal, L. (ed.) FOSSACS 2012. LNCS, vol. 7213, pp. 165–179. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  120. Stuber, J.: Superposition theorem proving for abelian groups represented as integer modules. Theoretical Computer Science 208(1-2), 149–177 (1998)

    Article  MathSciNet  MATH  Google Scholar 

  121. Stuber, J.: Superposition theorem proving for commutative rings. In: Bibel, W., Schmitt, P.H. (eds.) Automated Deduction - A Basis for Applications, vol. III. Applications, ch.2, pp. 31–55. Kluwer, Dordrecht (1998)

    Chapter  Google Scholar 

  122. Suda, M., Weidenbach, C.: A PLTL-Prover Based on Labelled Superposition with Partial Model Guidance. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol. 7364, pp. 537–543. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  123. Suda, M., Weidenbach, C., Wischnewski, P.: On the Saturation of YAGO. In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS (LNAI), vol. 6173, pp. 441–456. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  124. Waldmann, U.: Cancellative Superposition Decides the Theory of Divisible Torsion-free Abelian Groups. In: Ganzinger, H., McAllester, D., Voronkov, A. (eds.) LPAR 1999. LNCS (LNAI), vol. 1705, pp. 131–147. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  125. Waldmann, U.: Superposition and Chaining for Totally Ordered Divisible Abelian Groups. In: Goré, R., Leitsch, A., Nipkow, T. (eds.) EuroGP 2001. LNCS, vol. 2038, pp. 226–241. Springer, Heidelberg (2001), www.mpi-inf.mpg.de/~uwe/paper/IJCAR01-bibl.html

    Google Scholar 

  126. Weidenbach, C.: SPASS—version 0.49. Journal of Automated Reasoning 18(2), 247–252 (1997)

    Article  MathSciNet  Google Scholar 

  127. Weidenbach, C.: Towards an Automatic Analysis of Security Protocols in First-Order Logic. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 314–328. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  128. Wilhelm, R., Ripken, K., Ciesinger, J., Ganzinger, H., Lahner, W., Nollmann, R.: Design evaluation of the compiler generating system MUGI. In: Yeh, R.T., Ramamoorthy, C.V. (eds.) Proceedings of the 2nd International Conference on Software Engineering, San Francisco, California, USA, 1976, October 13-15, pp. 571–576. IEEE Computer Society (1976)

    Google Scholar 

  129. Wos, L., Robinson, G.A., Carson, D.F., Shalla, L.: The concept of demodulation in theorem proving. Journal of the ACM 14(4), 698–709 (1967)

    Article  MATH  Google Scholar 

  130. Weidenbach, C., Schmidt, R.A., Hillenbrand, T., Rusev, R., Topic, D.: System Description: Spass Version 3.0. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 514–520. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  131. Weidenbach, C., Wischnewski, P.: Subterm contextual rewriting. AI Communications 23(2-3), 97–109 (2010)

    MathSciNet  MATH  Google Scholar 

  132. Zhang, H.: Reduction, superposition and induction: Automated reasoning in an equational logic. Research Report 88–06, University of Iowa (November 1988)

    Google Scholar 

  133. Zhang, H., Kapur, D.: First-order Theorem Proving using Conditional Rewrite Rules. In: Lusk, E.‘., Overbeek, R. (eds.) CADE 1988. LNCS, vol. 310, pp. 1–20. Springer, Heidelberg (1988)

    Chapter  Google Scholar 

  134. Zhang, H., Kapur, D.: Consider only General Superpositions in Completion Procedures. In: Dershowitz, N. (ed.) RTA 1989. LNCS, vol. 355, pp. 513–527. Springer, Heidelberg (1989)

    Chapter  Google Scholar 

  135. Zhang, H., Kapur, D.: Unnecessary inferences in associative-commutative completion procedures. Mathematical Systems Theory 23(3), 175–206 (1990)

    Article  MathSciNet  MATH  Google Scholar 

  136. Zhang, H., Remy, J.-L.: Contextual Rewriting. In: Jouannaud, J.-P. (ed.) RTA 1985. LNCS, vol. 202, pp. 46–62. Springer, Heidelberg (1985)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of New Mexico, USA

    Deepak Kapur

  2. Technical University of Catalonia, Spain

    Robert Nieuwenhuis

  3. University of Manchester, UK

    Andrei Voronkov

  4. Max Planck Institute for Informatics, Germany

    Christoph Weidenbach

  5. Saarland University, Germany

    Reinhard Wilhelm

Authors
  1. Deepak Kapur
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Robert Nieuwenhuis
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Andrei Voronkov
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Christoph Weidenbach
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Reinhard Wilhelm
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. University of Manchester, Oxford Road, M13 9PL, Manchester, UK

    Andrei Voronkov

  2. Max-Planck-Institut für Informatik, Campus E1 4, 66123, Saarbrücken, Germany

    Christoph Weidenbach

Rights and permissions

Reprints and permissions

Copyright information

© 2013 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Kapur, D., Nieuwenhuis, R., Voronkov, A., Weidenbach, C., Wilhelm, R. (2013). Harald Ganzinger’s Legacy: Contributions to Logics and Programming. In: Voronkov, A., Weidenbach, C. (eds) Programming Logics. Lecture Notes in Computer Science, vol 7797. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-37651-1_1

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-37651-1_1

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-37650-4

  • Online ISBN: 978-3-642-37651-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation