×

Harald Ganzinger’s legacy: contributions to logics and programming. (English) Zbl 1383.68003

Voronkov, Andrei (ed.) et al., Programming logics. Essays in memory of Harald Ganzinger. Berlin: Springer (ISBN 978-3-642-37650-4/pbk). Lecture Notes in Computer Science 7797, 1-18 (2013).
Summary: 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.
For the entire collection see [Zbl 1259.03008].

MSC:

68-03 History of computer science
01A70 Biographies, obituaries, personalia, bibliographies
03B70 Logic in computer science
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)

Biographic References:

Ganzinger, Harald
PDFBibTeX XMLCite
Full Text: DOI

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) · Zbl 1367.68243 · doi:10.1145/1459010.1459014
[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) · Zbl 1193.03024 · doi:10.1007/978-3-642-04222-5_5
[3] Armando, A., Ranise, S., Rusinowitch, M.: A rewriting approach to satisfiability procedures. Information and Computation 183(2), 140–164 (2003) · Zbl 1054.68077 · doi:10.1016/S0890-5401(03)00020-8
[4] Bachmair, L., Dershowitz, N.: Critical pair criteria for completion. Journal of Symbolic Computation 6(1), 1–18 (1988) · Zbl 0651.68030 · doi:10.1016/S0747-7171(88)80018-X
[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) · doi:10.1007/3-540-51081-8_99
[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)
[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) · doi:10.1007/3-540-54317-1_89
[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) · doi:10.1007/3-540-52885-7_105
[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)
[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) · Zbl 0814.68117
[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) · Zbl 0925.03063 · doi:10.1007/BFb0013068
[12] Bachmair, L., Ganzinger, H.: Associative-commutative superposition. Technical Report MPI-I-93-267, Max-Planck-Institut für Informatik, Saarbrücken (December 1993) · Zbl 0924.03017
[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) · doi:10.1007/3-540-60381-6_1
[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) · doi:10.1007/BFb0016860
[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) · doi:10.1007/3-540-58156-1_32
[16] Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification. Journal of Logic and Computation 4(3), 217–247 (1994) · Zbl 0814.68117 · doi:10.1093/logcom/4.3.217
[17] Bachmair, L., Ganzinger, H.: Rewrite techniques for transitive relations. In: Ninth Annual IEEE Symposium on Logic in Computer Science, Paris, France (July 1994) · Zbl 0814.68117 · doi:10.1109/LICS.1994.316051
[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) · Zbl 1320.68163 · doi:10.1109/LICS.1996.561462
[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 · Zbl 1065.68615
[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) · Zbl 0973.68215
[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) · Zbl 0924.03017 · doi:10.1007/BFb0054258
[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) · Zbl 0993.03008 · doi:10.1016/B978-044450813-3/50004-7
[23] Basin, D.A., Ganzinger, H.: Automated complexity analysis based on ordered resolution. Journal of the ACM 48(1), 70–109 (2001) · Zbl 1320.68163 · doi:10.1145/363647.363681
[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)
[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) · Zbl 0925.03052
[26] Bachmair, L., Ganzinger, H., Lynch, C., Snyder, W.: Basic paramodulation. Information and Computation 121(2), 172–192 (1995) · Zbl 0833.68115 · doi:10.1006/inco.1995.1131
[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) · doi:10.1109/LICS.1999.782618
[28] Bertling, H., Ganzinger, H., Schäfers, R.: CEC: A system for conditional equational completion – User manual, version 1.0 (1988) · Zbl 0666.68015
[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) · Zbl 0666.68015 · doi:10.1007/3-540-19027-9_27
[30] Bertling, H., Ganzinger, H., Schäfers, R.: A collection of specifications completed by the CEC-system, version 1.0 (1988) · Zbl 0666.68015
[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) · doi:10.1007/BFb0014420
[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) · Zbl 0926.03006 · doi:10.1007/BFb0054259
[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) · Zbl 0925.03074 · doi:10.1007/BFb0013841
[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) · Zbl 0793.68127 · doi:10.1109/LICS.1993.287598
[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) · Zbl 0793.68127 · doi:10.1007/BFb0022557
[36] Bachmair, L., Ganzinger, H., Waldmann, U.: Refutational theorem proving for hierarchic first-order theories. Appl. Algebra Eng. Commun. Comput. 5, 193–212 (1994) · Zbl 0797.03008 · doi:10.1007/BF01190829
[37] Comon, H., Nieuwenhuis, R.: Induction = I-Axiomatization + First-Order Consistency. Information & Computation 159(1), 151–186 (2000) · Zbl 1046.68640 · doi:10.1006/inco.2000.2875
[38] Degtyarev, A., Fisher, M., Konev, B.: Monodic temporal resolution. ACM Trans. Comput. Log. 7(1), 108–150 (2006) · Zbl 1367.03035 · doi:10.1145/1119439.1119443
[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) · Zbl 1348.68218 · doi:10.1007/978-3-642-24364-6_9
[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) · Zbl 0328.68004
[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) · Zbl 0413.68082 · doi:10.1007/978-3-642-67444-0_19
[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) · Zbl 0413.68081 · doi:10.1007/3-540-09118-1_15
[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) · doi:10.1007/3-540-10250-7_18
[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) · doi:10.1007/978-3-662-01089-1_2
[45] Ganzinger, H.: Increasing modularity and language-independency in automatically generated compilers. Sci. Comput. Program. 3(3), 223–278 (1983) · Zbl 0565.68011 · doi:10.1016/0167-6423(83)90021-7
[46] Ganzinger, H.: Modular compiler descriptions based on abstract semantic data types. In: Proceedings 2nd Workshop on Abstract Data Types, University of Passau (1983) · Zbl 0516.68021
[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) · Zbl 0516.68021 · doi:10.1007/BFb0036912
[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) · Zbl 0511.68010 · doi:10.1145/2166.357212
[49] Ganzinger, H.: Knuth-Bendix completion for parametric specifications with conditional equations. In: Workshop on Specification of Abstract Data Types, ADT (1986)
[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) · Zbl 0666.68097 · doi:10.1007/3-540-19242-5_6
[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) · doi:10.1007/3-540-50325-0_4
[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) · Zbl 0612.68020 · doi:10.1007/BFb0039613
[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) · doi:10.1007/3-540-50939-9_136
[54] Ganzinger, H.: A Completion Procedure for Conditional Equations. Journal of Symbolic Computation 11, 51–81 (1991) · Zbl 0724.68053 · doi:10.1016/S0747-7171(08)80132-0
[55] Ganzinger, H.: Order-sorted completion: the many-sorted way. Theoretical Computer Science 89, 3–32 (1991) · Zbl 0736.68050 · doi:10.1016/0304-3975(90)90105-Q
[56] Ganzinger, H.: Shostak Light. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 332–346. Springer, Heidelberg (2002) · doi:10.1007/3-540-45620-1_28
[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) · doi:10.1109/LICS.1999.782624
[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) · doi:10.1145/800230.806993
[59] Ganzinger, H., Heeg, G., Baumeister, H., Rüger, M.: Smalltalk-80. Informationstechnik – IT 29(4), 241–251 (1987)
[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) · Zbl 0993.03017
[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) · Zbl 1103.68616 · doi:10.1007/978-3-540-27813-9_14
[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) · Zbl 1278.68260 · doi:10.1007/978-3-540-45085-6_15
[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) · Zbl 1319.68127 · doi:10.1142/S012905410000003X
[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) · doi:10.1109/LICS.2003.1210045
[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) · Zbl 1095.68111 · doi:10.1007/978-3-540-30124-0_9
[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) · Zbl 1165.03315 · doi:10.1007/11916277_34
[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) · doi:10.1109/LICS.1999.782582
[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) · doi:10.1007/3-540-63104-6_32
[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) · doi:10.1109/LICS.2000.855788
[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) · Zbl 0976.03518 · doi:10.1007/3-540-45406-3_4
[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) · doi:10.1109/LICS.2001.932481
[72] Godoy, G., Nieuwenhuis, R.: Superposition with Completely Built-in Abelian Groups. Journ. Symbolic Computation 37(1), 1–33 (2004) · Zbl 1043.03011 · doi:10.1016/S0747-7171(03)00070-1
[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) · Zbl 0988.68588 · doi:10.1007/3-540-45744-5_18
[75] Ganzinger, H., Nieuwenhuis, R., Nivela, P.: Fast term indexing with coded context trees. Journal of Automated Reasoning 32(2), 103–120 (2004) · Zbl 1073.68077 · doi:10.1023/B:JARS.0000029963.64213.ac
[76] Graf, P.: Substitution Tree Indexing. In: Hsiang, J. (ed.) RTA 1995. LNCS, vol. 914, pp. 117–131. Springer, Heidelberg (1995) · doi:10.1007/3-540-59200-8_52
[77] Ganzinger, H., Ripken, K., Wilhelm, R.: Automatic generation of optimizing multipass compilers. In: IFIP Congress, pp. 535–540 (1977) · Zbl 0363.68004
[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) · doi:10.1007/3-540-56393-8_17
[79] Ganzinger, H., Stuber, J.: Superposition with equivalence reasoning and delayed clause normal form transformation. Inf. Comput. 199(1-2), 3–23 (2005) · Zbl 1081.68092 · doi:10.1016/j.ic.2004.10.010
[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) · doi:10.1109/ISMVL.2000.848641
[81] Ganzinger, H., Sofronie-Stokkermans, V., Waldmann, U.: Modular proof systems for partial functions with Evans equality. Inf. Comput. 204(10), 1453–1492 (2006) · Zbl 1103.68112 · doi:10.1016/j.ic.2005.10.002
[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) · doi:10.1007/3-540-07410-4_666
[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) · doi:10.1007/3-540-56393-8_34
[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) · doi:10.1007/3-540-61511-3_102
[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)
[86] Hillenbrand, T.: Superposition and Decision Procedures – Back and Forth. PhD thesis, Universität des Saarlandes (2008)
[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) · Zbl 1291.68348 · doi:10.1007/978-3-642-14203-1_16
[88] Hustadt, U., Motik, B., Sattler, U.: Deciding expressive description logics in the framework of resolution. Inf. Comput. 206(5), 579–601 (2008) · Zbl 1146.68456 · doi:10.1016/j.ic.2007.11.006
[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)
[90] Horbach, M., Weidenbach, C.: Superposition for fixed domains. ACM Transactions on Computational Logic 11(4), 1–35 (2010) · Zbl 1351.03021 · doi:10.1145/1805950.1805957
[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) · Zbl 0903.03008 · doi:10.1007/BFb0052362
[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) · Zbl 1222.03046 · doi:10.1007/11814771_45
[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) · Zbl 0188.04902 · doi:10.1016/B978-0-08-012975-4.50028-X
[94] Kirchner, C., Kirchner, H., Rusinowitch, M.: Deduction with symbolic constraints. Revue Française d’Intelligence Artificielle 4(3), 9–52 (1990)
[95] Kazakov, Y., Motik, B.: A resolution-based decision procedure for shoiq. Journal of Automated Reasoning 40(2-3), 89–116 (2008) · Zbl 1137.68056 · doi:10.1007/s10817-007-9090-1
[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) · Zbl 0651.68029 · doi:10.1016/S0747-7171(88)80019-1
[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) · Zbl 1179.03018 · doi:10.1007/978-3-540-74915-8_19
[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) · Zbl 1213.68572 · doi:10.1007/978-3-540-73595-3_21
[99] Lynch, C., Snyder, W.: Redundancy criteria for constrained completion. Theoretical Compututer Science 142(2), 141–177 (1995) · Zbl 0873.68189 · doi:10.1016/0304-3975(94)00274-6
[100] Levy, J., Veanes, M.: On the undecidability of second-order unification. Inf. Comput. 159(1-2), 125–150 (2000) · Zbl 1005.03007 · doi:10.1006/inco.2000.2877
[101] McAllester, D.: Automatic recognition of tractability in inferences relations. Journal of the ACM 40(2), 284–303 (1993) · Zbl 0770.68106 · doi:10.1145/151261.151265
[102] McCune, W.: Solution of the Robbins problem. Journal of Automated Reasoning 19(3), 263–276 (1997) · Zbl 0883.06011 · doi:10.1023/A:1005843212881
[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) · Zbl 1278.68184 · doi:10.1007/978-3-540-45069-6_1
[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) · doi:10.1109/LICS.1996.561464
[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) · doi:10.1007/3-540-61511-3_125
[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) · doi:10.1007/3-540-56868-9_33
[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) · doi:10.1007/3-540-55253-7_22
[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) · Zbl 0925.03076 · doi:10.1007/3-540-55602-8_186
[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) · doi:10.1007/3-540-58156-1_40
[110] Nieuwenhuis, R., Rubio, A.: Theorem Proving with Ordering and Equality Constrained Clauses. Journal of Symbolic Computation 19(4), 321–351 (1995) · Zbl 0844.68107 · doi:10.1006/jsco.1995.1020
[111] Peterson, G.E.: A technique for establishing completeness results in theorem proving with equality. SIAM J. on Computing 12(1), 82–100 (1983) · Zbl 0522.68087 · doi:10.1137/0212006
[112] Robinson, J.A.: A machine-oriented logic based on the resolution principle. Journal of the ACM 12(1), 23–41 (1965) · Zbl 0139.12303 · doi:10.1145/321250.321253
[113] Riazanov, A., Voronkov, A.: The design and implementation of VAMPIRE. AI Communications 15(91-110) (2002) · Zbl 1021.68082
[114] Robinson, G.A., Wos, L.T.: Paramodulation and theorem-proving in first order theories with equality. Machine Intelligence 4, 135–150 (1969) · Zbl 0219.68047
[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)
[116] Stephan Schulz, E.: A Brainiac Theorem Prover. Journal of AI Communications 15(2/3), 111–126 (2002) · Zbl 1020.68084
[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) · Zbl 0963.03006 · doi:10.1007/10721959_34
[118] Schmidt, R.A., Hustadt, U.: The axiomatic translation principle for modal logic. ACM Trans. Comput. Log. 8(4), 1–51 (2007) · Zbl 1367.03045 · doi:10.1145/1276920.1276921
[119] Seidl, H., Reuß, A.: Extending \({\mathcal H}_1\) -Clauses with Path Disequalities. In: Birkedal, L. (ed.) FOSSACS 2012. LNCS, vol. 7213, pp. 165–179. Springer, Heidelberg (2012) · Zbl 1352.68118 · doi:10.1007/978-3-642-28729-9_11
[120] Stuber, J.: Superposition theorem proving for abelian groups represented as integer modules. Theoretical Computer Science 208(1-2), 149–177 (1998) · Zbl 0912.68187 · doi:10.1016/S0304-3975(98)00082-6
[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) · Zbl 0970.03022 · doi:10.1007/978-94-017-0437-3_2
[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) · Zbl 1358.68266 · doi:10.1007/978-3-642-31365-3_42
[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) · Zbl 1291.68372 · doi:10.1007/978-3-642-14203-1_38
[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) · Zbl 0939.03014 · doi:10.1007/3-540-48242-3_9
[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 · Zbl 0988.03510 · doi:10.1007/3-540-45744-5_17
[126] Weidenbach, C.: SPASS–version 0.49. Journal of Automated Reasoning 18(2), 247–252 (1997) · Zbl 05468578 · doi:10.1023/A:1005812220011
[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) · Zbl 1038.94548 · doi:10.1007/3-540-48660-7_29
[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)
[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) · Zbl 0157.02501 · doi:10.1145/321420.321429
[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) · Zbl 1213.68577 · doi:10.1007/978-3-540-73595-3_38
[131] Weidenbach, C., Wischnewski, P.: Subterm contextual rewriting. AI Communications 23(2-3), 97–109 (2010) · Zbl 1206.68164
[132] Zhang, H.: Reduction, superposition and induction: Automated reasoning in an equational logic. Research Report 88–06, University of Iowa (November 1988)
[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) · Zbl 0645.68096 · doi:10.1007/BFb0012820
[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) · doi:10.1007/3-540-51081-8_129
[135] Zhang, H., Kapur, D.: Unnecessary inferences in associative-commutative completion procedures. Mathematical Systems Theory 23(3), 175–206 (1990) · Zbl 0707.68071 · doi:10.1007/BF02090774
[136] Zhang, H., Remy, J.-L.: Contextual Rewriting. In: Jouannaud, J.-P. (ed.) RTA 1985. LNCS, vol. 202, pp. 46–62. Springer, Heidelberg (1985) · Zbl 0576.68012 · doi:10.1007/3-540-15976-2_2
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.