×

zbMATH — the first resource for mathematics

Ganzinger, Harald

Compute Distance To:
Author ID: ganzinger.harald Recent zbMATH articles by "Ganzinger, Harald"
Published as: Ganzinger, H.; Ganzinger, Harald
External Links: MGP · Wikidata · dblp · GND
Documents Indexed: 64 Publications since 1975, including 9 Books
Biographic References: 4 Publications

Publications by Year

Citations contained in zbMATH Open

49 Publications have been cited 477 times in 313 Documents Cited by Year
Resolution theorem proving. Zbl 0993.03008
Bachmair, Leo; Ganzinger, Harald
75
2001
Rewrite-based equational theorem proving with selection and simplification. Zbl 0814.68117
Bachmair, Leo; Ganzinger, Harald
70
1994
DPLL(\(T\)): Fast decision procedures. Zbl 1103.68616
Ganzinger, Harald; Hagen, George; Nieuwenhuis, Robert; Oliveras, Albert; Tinelli, Cesare
39
2004
Superposition with simplification as a decision procedure for the monadic class with equality. Zbl 0793.68127
Bachmair, Leo; Ganzinger, Harald; Waldmann, Uwe
28
1993
Refutational theorem proving for hierarchic first-order theories. Zbl 0797.03008
Bachmair, Leo; Ganzinger, Harald; Waldmann, Uwe
21
1994
Basic paramodulation. Zbl 0833.68115
Bachmair, Leo; Ganzinger, Harald; Lynch, Christopher; Snyder, Wayne
18
1995
Ordered chaining calculi for first-order theories of transitive relations. Zbl 1065.68615
Bachmair, Leo; Ganzinger, Harald
17
1998
Parameterized specifications: Parameter passing and imlementation with respect to observability. Zbl 0511.68010
Ganzinger, Harald
17
1983
Basic paramodulation and superposition. Zbl 0925.03052
Bachmair, Leo; Ganzinger, Harald; Lynch, Christopher; Snyder, Wayne
16
1992
Automated complexity analysis based on ordered resolution. Zbl 1320.68163
Basin, David; Ganzinger, Harald
13
2001
Equational reasoning in saturation-based theorem proving. Zbl 0973.68215
Bachmair, Leo; Ganzinger, Harald
13
1998
Increasing modularity and language-independency in automatically generated compilers. Zbl 0565.68011
Ganzinger, Harald
12
1983
Modular proof systems for partial functions with Evans equality. Zbl 1103.68112
Ganzinger, Harald; Sofronie-Stokkermans, Viorica; Waldmann, Uwe
10
2006
Order-sorted completion: The many-sorted way. Zbl 0736.68050
Ganzinger, Harald
10
1991
Theory instantiation. Zbl 1165.03315
Ganzinger, Harald; Korovin, Konstantin
9
2006
Integrating equational reasoning into instantiation-based theorem proving. Zbl 1095.68111
Ganzinger, Harald; Korovin, Konstantin
9
2004
A completion procedure for conditional equations. Zbl 0724.68053
Ganzinger, Harald
9
1991
Ground term confluence in parametric conditional equational specifications. Zbl 0612.68020
Ganzinger, Harald
9
1987
Shostak light. Zbl 1072.68572
Ganzinger, Harald
6
2002
A resolution-based decision procedure for extensions of K4. Zbl 0993.03017
Ganzinger, Harald; Hustadt, Ullrich; Meyer, Christoph; Schmidt, Renate A.
6
2001
Rigid reachability. Zbl 0928.03002
Ganzinger, Harald; Jacquemard, Florent; Veanes, Margus
5
1998
Modular proof systems for partial functions with weak equality. Zbl 1126.68564
Ganzinger, Harald; Sofronie-Stokkermans, Viorica; Waldmann, Uwe
4
2004
Superposition with equivalence reasoning and delayed clause normal form transformation. Zbl 1278.68261
Ganzinger, Harald; Stuber, Jürgen
4
2003
Nonclausal resolution and superposition with selection and redundancy criteria. Zbl 0925.03063
Bachmair, Leo; Ganzinger, Harald
4
1992
CEC: A system for the completion of conditional equational specifications. Zbl 0666.68015
Bertling, Hubert; Ganzinger, Harald; Schäfers, Renate
4
1988
On storage optimization for automatically generated compilers. Zbl 0413.68081
Ganzinger, Harald
4
1979
Logical algorithms. Zbl 1045.68061
Ganzinger, Harald; McAllester, David
3
2002
Context trees. Zbl 0988.68588
Ganzinger, Harald; Nieuwenhuis, Robert; Nivela, Pilar
3
2001
Constraints and theorem proving. Zbl 0976.03518
Ganzinger, Harald; Nieuwenhuis, Robert
3
2001
Elimination of equality via transformation with ordering constraints. Zbl 0926.03006
Bachmair, Leo; Ganzinger, Harald; Voronkov, Andrei
3
1998
Strict basic superposition. Zbl 0924.03017
Bachmair, Leo; Ganzinger, Harald
3
1998
Theorem proving in cancellative abelian monoids (extended abstract). Zbl 1412.68225
Ganzinger, Harald; Waldmann, Uwe
3
1996
Automatic generation of optimizing multipass compilers. Zbl 0363.68004
Ganzinger, Harald; Ripken, Knut; Wilhelm, Reinhard
3
1977
Superposition with equivalence reasoning and delayed clause normal form transformation. Zbl 1081.68092
Ganzinger, Harald; Stuber, Jürgen
2
2005
Superposition modulo a Shostak theory. Zbl 1278.68260
Ganzinger, Harald; Hillenbrand, Thomas; Waldmann, Uwe
2
2003
Rigid reachability, the non-symmetric form of rigid E-unification. Zbl 1319.68127
Ganzinger, Harald; Jacquemard, Florent; Veanes, Margus
2
2000
Decidable fragments of simultaneous rigid reachability. Zbl 0943.68096
Cortier, Veronique; Ganzinger, Harald; Jacquemard, Florent; Veanes, Margus
2
1999
Theorem proving for hierarchic first-order theories. Zbl 0925.03074
Bachmair, Leo; Ganzinger, Harald; Waldmann, Uwe
2
1992
A completion procedure for conditional equations. Zbl 0666.68097
Ganzinger, Harald
2
1988
Completion with history-dependent complexities for generated equations. Zbl 0659.68049
Ganzinger, Harald
2
1988
Programs as data objects. Proceedings of a Workshop, Copenhagen, Denmark, October 17–19, 1985. Zbl 0578.00007
Ganzinger, Harald (ed.); Jones, Neil D. (ed.)
2
1986
Fast term indexing with coded context trees. Zbl 1073.68077
Ganzinger, Harald; Nieuwenhuis, Robert; Nivela, Pilar
1
2004
Automated deduction - CADE-16. 16th international conference, Trento, Italy, July 7–10, 1999. Proceedings. Zbl 0917.00015
Ganzinger, Harald (ed.)
1
1999
Rewriting techniques and applications. 7th international conference, RTA ’96, New Brunswick, NJ, USA, July 27-30, 1996. Proceedings. Zbl 1102.68309
Ganzinger, Harald (ed.)
1
1996
A note on the termination in combinations of heterogeneous term rewriting systems. Zbl 1023.68593
Ganzinger, Harald; Giegerich, Robert
1
1987
Modular compiler descriptions based on abstract semantic data types (extended abstract). Zbl 0516.68021
Ganzinger, Harald
1
1983
Denotational semantics for languages with modules. Zbl 0512.68010
Ganzinger, Harald
1
1983
An approach to the derivation of compiler description concepts from the mathematical semantics concept. Zbl 0413.68082
Ganzinger, H.
1
1979
Darstellung der Artanpassung in höheren Programmiersprachen durch Repräsentationen von Gruppen. Zbl 0328.68004
Ganzinger, Harald
1
1976
Modular proof systems for partial functions with Evans equality. Zbl 1103.68112
Ganzinger, Harald; Sofronie-Stokkermans, Viorica; Waldmann, Uwe
10
2006
Theory instantiation. Zbl 1165.03315
Ganzinger, Harald; Korovin, Konstantin
9
2006
Superposition with equivalence reasoning and delayed clause normal form transformation. Zbl 1081.68092
Ganzinger, Harald; Stuber, Jürgen
2
2005
DPLL(\(T\)): Fast decision procedures. Zbl 1103.68616
Ganzinger, Harald; Hagen, George; Nieuwenhuis, Robert; Oliveras, Albert; Tinelli, Cesare
39
2004
Integrating equational reasoning into instantiation-based theorem proving. Zbl 1095.68111
Ganzinger, Harald; Korovin, Konstantin
9
2004
Modular proof systems for partial functions with weak equality. Zbl 1126.68564
Ganzinger, Harald; Sofronie-Stokkermans, Viorica; Waldmann, Uwe
4
2004
Fast term indexing with coded context trees. Zbl 1073.68077
Ganzinger, Harald; Nieuwenhuis, Robert; Nivela, Pilar
1
2004
Superposition with equivalence reasoning and delayed clause normal form transformation. Zbl 1278.68261
Ganzinger, Harald; Stuber, Jürgen
4
2003
Superposition modulo a Shostak theory. Zbl 1278.68260
Ganzinger, Harald; Hillenbrand, Thomas; Waldmann, Uwe
2
2003
Shostak light. Zbl 1072.68572
Ganzinger, Harald
6
2002
Logical algorithms. Zbl 1045.68061
Ganzinger, Harald; McAllester, David
3
2002
Resolution theorem proving. Zbl 0993.03008
Bachmair, Leo; Ganzinger, Harald
75
2001
Automated complexity analysis based on ordered resolution. Zbl 1320.68163
Basin, David; Ganzinger, Harald
13
2001
A resolution-based decision procedure for extensions of K4. Zbl 0993.03017
Ganzinger, Harald; Hustadt, Ullrich; Meyer, Christoph; Schmidt, Renate A.
6
2001
Context trees. Zbl 0988.68588
Ganzinger, Harald; Nieuwenhuis, Robert; Nivela, Pilar
3
2001
Constraints and theorem proving. Zbl 0976.03518
Ganzinger, Harald; Nieuwenhuis, Robert
3
2001
Rigid reachability, the non-symmetric form of rigid E-unification. Zbl 1319.68127
Ganzinger, Harald; Jacquemard, Florent; Veanes, Margus
2
2000
Decidable fragments of simultaneous rigid reachability. Zbl 0943.68096
Cortier, Veronique; Ganzinger, Harald; Jacquemard, Florent; Veanes, Margus
2
1999
Automated deduction - CADE-16. 16th international conference, Trento, Italy, July 7–10, 1999. Proceedings. Zbl 0917.00015
Ganzinger, Harald (ed.)
1
1999
Ordered chaining calculi for first-order theories of transitive relations. Zbl 1065.68615
Bachmair, Leo; Ganzinger, Harald
17
1998
Equational reasoning in saturation-based theorem proving. Zbl 0973.68215
Bachmair, Leo; Ganzinger, Harald
13
1998
Rigid reachability. Zbl 0928.03002
Ganzinger, Harald; Jacquemard, Florent; Veanes, Margus
5
1998
Elimination of equality via transformation with ordering constraints. Zbl 0926.03006
Bachmair, Leo; Ganzinger, Harald; Voronkov, Andrei
3
1998
Strict basic superposition. Zbl 0924.03017
Bachmair, Leo; Ganzinger, Harald
3
1998
Theorem proving in cancellative abelian monoids (extended abstract). Zbl 1412.68225
Ganzinger, Harald; Waldmann, Uwe
3
1996
Rewriting techniques and applications. 7th international conference, RTA ’96, New Brunswick, NJ, USA, July 27-30, 1996. Proceedings. Zbl 1102.68309
Ganzinger, Harald (ed.)
1
1996
Basic paramodulation. Zbl 0833.68115
Bachmair, Leo; Ganzinger, Harald; Lynch, Christopher; Snyder, Wayne
18
1995
Rewrite-based equational theorem proving with selection and simplification. Zbl 0814.68117
Bachmair, Leo; Ganzinger, Harald
70
1994
Refutational theorem proving for hierarchic first-order theories. Zbl 0797.03008
Bachmair, Leo; Ganzinger, Harald; Waldmann, Uwe
21
1994
Superposition with simplification as a decision procedure for the monadic class with equality. Zbl 0793.68127
Bachmair, Leo; Ganzinger, Harald; Waldmann, Uwe
28
1993
Basic paramodulation and superposition. Zbl 0925.03052
Bachmair, Leo; Ganzinger, Harald; Lynch, Christopher; Snyder, Wayne
16
1992
Nonclausal resolution and superposition with selection and redundancy criteria. Zbl 0925.03063
Bachmair, Leo; Ganzinger, Harald
4
1992
Theorem proving for hierarchic first-order theories. Zbl 0925.03074
Bachmair, Leo; Ganzinger, Harald; Waldmann, Uwe
2
1992
Order-sorted completion: The many-sorted way. Zbl 0736.68050
Ganzinger, Harald
10
1991
A completion procedure for conditional equations. Zbl 0724.68053
Ganzinger, Harald
9
1991
CEC: A system for the completion of conditional equational specifications. Zbl 0666.68015
Bertling, Hubert; Ganzinger, Harald; Schäfers, Renate
4
1988
A completion procedure for conditional equations. Zbl 0666.68097
Ganzinger, Harald
2
1988
Completion with history-dependent complexities for generated equations. Zbl 0659.68049
Ganzinger, Harald
2
1988
Ground term confluence in parametric conditional equational specifications. Zbl 0612.68020
Ganzinger, Harald
9
1987
A note on the termination in combinations of heterogeneous term rewriting systems. Zbl 1023.68593
Ganzinger, Harald; Giegerich, Robert
1
1987
Programs as data objects. Proceedings of a Workshop, Copenhagen, Denmark, October 17–19, 1985. Zbl 0578.00007
Ganzinger, Harald (ed.); Jones, Neil D. (ed.)
2
1986
Parameterized specifications: Parameter passing and imlementation with respect to observability. Zbl 0511.68010
Ganzinger, Harald
17
1983
Increasing modularity and language-independency in automatically generated compilers. Zbl 0565.68011
Ganzinger, Harald
12
1983
Modular compiler descriptions based on abstract semantic data types (extended abstract). Zbl 0516.68021
Ganzinger, Harald
1
1983
Denotational semantics for languages with modules. Zbl 0512.68010
Ganzinger, Harald
1
1983
On storage optimization for automatically generated compilers. Zbl 0413.68081
Ganzinger, Harald
4
1979
An approach to the derivation of compiler description concepts from the mathematical semantics concept. Zbl 0413.68082
Ganzinger, H.
1
1979
Automatic generation of optimizing multipass compilers. Zbl 0363.68004
Ganzinger, Harald; Ripken, Knut; Wilhelm, Reinhard
3
1977
Darstellung der Artanpassung in höheren Programmiersprachen durch Repräsentationen von Gruppen. Zbl 0328.68004
Ganzinger, Harald
1
1976
all top 5

Cited by 405 Authors

17 Weidenbach, Christoph
12 Waldmann, Uwe
10 Bonacina, Maria Paola
10 Peltier, Nicolas
9 Baumgartner, Peter
9 Hustadt, Ullrich
9 Nieuwenhuis, Robert
8 Ranise, Silvio
8 Voronkov, Andrei
7 Blanchette, Jasmin Christian
7 Ganzinger, Harald
7 Lynch, Christopher A.
7 Schmidt, Renate A.
7 Sofronie-Stokkermans, Viorica
7 Tinelli, Cesare
6 Meseguer Guaita, José
6 Motik, Boris
5 Echenim, Mnacho
5 Engelfriet, Joost
5 Kirchner, Hélène
5 Ringeissen, Christophe
5 Sannella, Donald T.
5 Tarlecki, Andrzej
4 Barrett, Clark W.
4 de Moura, Leonardo
4 Dershowitz, Nachum
4 Dixon, Clare
4 Fontaine, Pascal
4 Ghilardi, Silvio
4 Goubault-Larrecq, Jean
4 Guller, Dušan
4 Kirchner, Claude
4 Reynolds, Andrew
4 Rusinowitch, Michaël
4 Tran, Duc-Khanh
3 Böhme, Sascha
3 Bouhoula, Adel
3 Bruttomesso, Roberto
3 Cimatti, Alessandro
3 de Nivelle, Hans
3 Degtyarev, Anatoli Ivanovich
3 Fleury, Mathias
3 Hähnle, Reiner
3 Hillenbrand, Thomas
3 Horbach, Matthias
3 Horrocks, Ian
3 Jacquemard, Florent
3 Kerber, Manfred
3 Kozen, Dexter C.
3 Kruglov, Evgeniĭ Valentinovich
3 Maneth, Sebastian
3 Orejas, Fernando
3 Paulson, Lawrence Charles
3 Plaisted, David Alan
3 Rubio, Albert
3 Sebastiani, Roberto
3 Sorge, Volker
3 Suda, Martin
3 Veanes, Margus
3 Zhang, Lan
2 Areces, Carlos
2 Badban, Bahareh
2 Banković, Milan
2 Benzmüller, Christoph Ewald
2 Beyersdorff, Olaf
2 Bidoit, Michel
2 Bozzano, Marco
2 Bright, Curtis
2 Caferra, Ricardo
2 Charatonik, Witold
2 Chew, Leroy
2 Chocron, Paula Daniela
2 Christ, Jürgen
2 Ciabattoni, Agata
2 Comon-Lundh, Hubert
2 Conchon, Sylvain
2 Déharbe, David
2 Eggers, Andreas
2 Fietzke, Arnaud
2 Ganesh, Vijay
2 Giegerich, Robert
2 Godoy, Guillem
2 Griggio, Alberto
2 Hintermeier, Claus
2 Hoenicke, Jochen
2 Jamnik, Mateja
2 Jouannaud, Jean-Pierre
2 Junttila, Tommi A.
2 Kapur, Deepak
2 Kazakov, Yevgeny
2 Kohlhase, Michael
2 Korovin, Konstantin
2 Kotsireas, Ilias S.
2 Kovács, Laura Ildikó
2 Kröning, Daniel
2 Levy, Jordi
2 Maletti, Andreas
2 Meier, Andreas
2 Nagashima, Masanori
2 Navarro, Marisa
...and 305 more Authors

Citations by Year

Wikidata Timeline

The data are displayed as stored in Wikidata under a Creative Commons CC0 License. Updates and corrections should be made in Wikidata.