dblp.uni-trier.dewww.uni-trier.de

Harald Ganzinger Vis

List of publications from the DBLP Bibliography Server - FAQ
Coauthor Index - Ask others: ACM DL/Guide - CiteSeerX - CSB - MetaPress - Google - Bing - Yahoo
Home Page

*2006
95EEHarald Ganzinger, Konstantin Korovin: Theory Instantiation. LPAR 2006: 497-511
94EEHarald Ganzinger, Viorica Sofronie-Stokkermans, Uwe Waldmann: Modular proof systems for partial functions with Evans equality. Inf. Comput. 204(10): 1453-1492 (2006)
2005
93EEHarald Ganzinger, Jürgen Stuber: Superposition with equivalence reasoning and delayed clause normal form transformation. Inf. Comput. 199(1-2): 3-23 (2005)
2004
92EEHarald Ganzinger, George Hagen, Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli: DPLL( T): Fast Decision Procedures. CAV 2004: 175-188
91EEHarald Ganzinger, Konstantin Korovin: Integrating Equational Reasoning into Instantiation-Based Theorem Proving. CSL 2004: 71-84
90EEHarald Ganzinger, Viorica Sofronie-Stokkermans, Uwe Waldmann: Modular Proof Systems for Partial Functions with Weak Equality. IJCAR 2004: 168-182
89EEHarald Ganzinger, Robert Nieuwenhuis, Pilar Nivela: Fast Term Indexing with Coded Context Trees. J. Autom. Reasoning 32(2): 103-120 (2004)
2003
88EEHarald Ganzinger, Thomas Hillenbrand, Uwe Waldmann: Superposition Modulo a Shostak Theory. CADE 2003: 182-196
87EEHarald Ganzinger, Jürgen Stuber: Superposition with Equivalence Reasoning and Delayed Clause Normal Form Transformation. CADE 2003: 335-349
86EEHarald Ganzinger, Konstantin Korovin: New Directions in Instantiation-Based Theorem Proving. LICS 2003: 55-64
2002
85EEHarald Ganzinger: Shostak Light. CADE 2002: 332-346
84EEHarald Ganzinger, David A. McAllester: Logical Algorithms. ICLP 2002: 209-223
2001
83EEHarald Ganzinger, Robert Nieuwenhuis, Pilar Nivela: Context Trees. IJCAR 2001: 242-256
82EEHarald Ganzinger, David A. McAllester: A New Meta-complexity Theorem for Bottom-Up Logic Programs. IJCAR 2001: 514-528
81 Harald Ganzinger: Relating Semantic and Proof-Theoretic Concepts for Polynominal Time Decidability of Uniform Word Problems. LICS 2001: 81-92
80EEHarald Ganzinger: Bottom-Up Deduction with Deletion and Priorities. PADO 2001: 276-278
79EEHarald Ganzinger: Efficient deductive methods for program analysis. POPL 2001: 102-103
78 Leo Bachmair, Harald Ganzinger: Resolution Theorem Proving. Handbook of Automated Reasoning 2001: 19-99
77EEDavid A. Basin, Harald Ganzinger: Automated complexity analysis based on ordered resolution. J. ACM 48(1): 70-109 (2001)
2000
76EEHarald Ganzinger, Viorica Sofronie-Stokkermans: Chaining Techniques for Automated Theorem Proving in Many-Valued Logics. ISMVL 2000: 337-344
75 Harald Ganzinger, Florent Jacquemard, Margus Veanes: Rigid Reachability, The Non-Symmetric Form of Rigid E-Unification. Int. J. Found. Comput. Sci. 11(1): 3-27 (2000)
1999
74 Harald Ganzinger: Automated Deduction - CADE-16, 16th International Conference on Automated Deduction, Trento, Italy, July 7-10, 1999, Proceedings Springer 1999
73 Harald Ganzinger, David A. McAllester, Andrei Voronkov: Logic Programming and Automated Reasoning, 6th International Conference, LPAR'99, Tbilisi, Georgia, September 6-10, 1999, Proceedings Springer 1999
72EEHarald Ganzinger, Robert Nieuwenhuis: Constraints and Theorem Proving. CCL 1999: 159-201
71EEVéronique Cortier, Harald Ganzinger, Florent Jacquemard, Margus Veanes: Decidable Fragments of Simultaneous Rigid Reachability. ICALP 1999: 250-260
70EEHarald Ganzinger, Christoph Meyer, Margus Veanes: The Two-Variable Guarded Fragment with Transitive Relations. LICS 1999: 24-34
69EEHarald Ganzinger, Hans de Nivelle: A Superposition Decision Procedure for the Guarded Fragment with Equality. LICS 1999: 295-304
1998
68EEHarald Ganzinger, Florent Jacquemard, Margus Veanes: Rigid Reachability. ASIAN 1998: 4-21
67 Harald Ganzinger, Ullrich Hustadt, Christoph Meyer, Renate A. Schmidt: A Resolution-Based Decision Procedure for Extensions of K4. Advances in Modal Logic 1998: 225-246
66EELeo Bachmair, Harald Ganzinger: Strict Basic Superposition. CADE 1998: 160-174
65EELeo Bachmair, Harald Ganzinger, Andrei Voronkov: Elimination of Equality via Transformation with Ordering Constraints. CADE 1998: 175-190
64EELeo Bachmair, Harald Ganzinger: Ordered Chaining Calculi for First-Order Theories of Transitive Relations. J. ACM 45(6): 1007-1049 (1998)
63 Harald Ganzinger, Jörg H. Siekmann, Peter H. Schmitt: Wohin geht die automatische Deduktion? KI 12(4): 33-37 (1998)
1997
62EEHarald Ganzinger, Christoph Meyer, Christoph Weidenbach: Soft Typing for Ordered Resolution. CADE 1997: 321-335
1996
61 Harald Ganzinger: Rewriting Techniques and Applications, 7th International Conference, RTA-96, New Brunswick, NJ, USA, July 27-30, 1996, Proceedings Springer 1996
60EEHarald Ganzinger: Saturation-Based Theorem Proving: Past Successes and Future Potential (Abstract). CADE 1996: 1
59EEHarald Ganzinger, Uwe Waldmann: Theorem Proving in Cancellative Abelian Monoids (Extended Abstract). CADE 1996: 388-402
58EEHarald Ganzinger: Saturation-Based Theorem Proving (Abstract). ICALP 1996: 1-3
57 David A. Basin, Harald Ganzinger: Complexity Analysis Based on Ordered Resolution. LICS 1996: 456-465
1995
56 Leo Bachmair, Harald Ganzinger, Christopher Lynch, Wayne Snyder: Basic Paramodulation Inf. Comput. 121(2): 172-192 (1995)
1994
55EELeo Bachmair, Harald Ganzinger: Ordered Chaining for Total Orderings. CADE 1994: 435-450
54 Leo Bachmair, Harald Ganzinger: Buchberger's Algorithm: A Constraint-Based Completion Procedure. CCL 1994: 285-301
53 Leo Bachmair, Harald Ganzinger, Jürgen Stuber: Combining Algebra and Universal Algebra in First-Order Theorem Proving: The Case of Commutative Rings. COMPASS/ADT 1994: 1-29
52 Leo Bachmair, Harald Ganzinger: Associative-Commutative Superposition. CTRS 1994: 1-14
51 Leo Bachmair, Harald Ganzinger: Rewrite Techniques for Transitive Relations LICS 1994: 384-393
50 Leo Bachmair, Harald Ganzinger, Uwe Waldmann: Refutational Theorem Proving for Hierachic First-Order Theories. Appl. Algebra Eng. Commun. Comput. 5: 193-212 (1994)
49 Leo Bachmair, Harald Ganzinger: Rewrite-Based Equational Theorem Proving with Selection and Simplification. J. Log. Comput. 4(3): 217-247 (1994)
1993
48 Leo Bachmair, Harald Ganzinger, Uwe Waldmann: Superposition with Simplification as a Desision Procedure for the Monadic Class with Equality. Kurt Gödel Colloquium 1993: 83-96
47 Leo Bachmair, Harald Ganzinger, Uwe Waldmann: Set Constraints are the Monadic Class LICS 1993: 75-83
46 Hubert Bertling, Harald Ganzinger, Renate Schäfers, Robert Nieuwenhuis, Fernando Orejas: Program Development: Completion Subsystem. PROSPECTRA Book 1993: 460-494
1992
45EELeo Bachmair, Harald Ganzinger, Uwe Waldmann: Theorem Proving for Hierarchic First-Order Theories. ALP 1992: 420-434
44EELeo Bachmair, Harald Ganzinger, Christopher Lynch, Wayne Snyder: Basic Paramodulation and Superposition. CADE 1992: 462-476
43 Harald Ganzinger, Jürgen Stuber: Inductive Theorem Proving by Consistency for First-Order Clauses. CTRS 1992: 226-241
42 Harald Ganzinger, Uwe Waldmann: Termination Proofs of Well-Moded Logic Programs via Conditional Rewrite Systems. CTRS 1992: 430-437
41EELeo Bachmair, Harald Ganzinger: Non-Clausal Resolution and Superposition with Selection and Redundancy Criteria. LPAR 1992: 273-284
40 Harald Ganzinger: Konferenzbericht LICS '92. KI 6(3): 51 (1992)
1991
39 Leo Bachmair, Harald Ganzinger: Perfect Model Semantics for Logic Programs with Equality. ICLP 1991: 645-659
38 Harald Ganzinger: A Completion Procedure for Conditional Equations. J. Symb. Comput. 11(1/2): 51-81 (1991)
37 Harald Ganzinger: Order-Sorted Completion: The Many-Sorted Way. Theor. Comput. Sci. 89(1): 3-32 (1991)
1990
36EELeo Bachmair, Harald Ganzinger: On Restrictions of Ordered Paramodulation with Simplification. CADE 1990: 427-441
35 Leo Bachmair, Harald Ganzinger: Completion of First-Order Clauses with Equality by Strict Superposition (Extended Abstract). CTRS 1990: 162-180
34 Harald Ganzinger, Renate Schäfers: System Support for Modular Order-Sorted Horn Clause Specifications. ICSE 1990: 150-159
1989
33EEHubert Bertling, Harald Ganzinger: Completion-Time Optimization of Rewrite-Time Goal Solving. RTA 1989: 45-58
32EEHarald Ganzinger: Order-Sorted Completion: The Many-Sorted Way (Extended Abstract). TAPSOFT, Vol.1 1989: 244-258
1988
31 Harald Ganzinger: ESOP '88, 2nd European Symposium on Programming, Nancy, France, March 21-24, 1988, Proceedings Springer 1988
30EEHubert Bertling, Harald Ganzinger, Renate Schäfers: CEC: A System for the Completion of Conditional Equational Specifications. ESOP 1988: 378-379
1987
29 Harald Ganzinger: Completion with History-Dependent Complexities for Generated Equations. ADT 1987: 73-91
28 Hubert Bertling, Harald Ganzinger, Renate Schäfers: A Systems for the Completion of Conditional Equational Specifications. CTRS 1987: 249-250
27 Harald Ganzinger: A Completion Procedure for Conditional Equations. CTRS 1987: 62-83
26EEHarald Ganzinger: Ground Term Confluence in Parametric Conditional Equational Specifications. STACS 1987: 286-298
25 Hubert Bertling, Harald Ganzinger, Hubert Baumeister: CEC (Conditional Equations Completion). STACS 1987: 470
24 Harald Ganzinger, Robert Giegerich: A note on termination in combinatiosn of heterogeneous term rewriting systems. Bulletin of the EATCS 31: 22-27 (1987)
1986
23 Harald Ganzinger, Neil D. Jones: Programs as Data Objects, Proceedings of a Workshop, Copenhagen, Denmark, October 17-19, 1985 Springer 1986
22 Harald Ganzinger: Knuth-Bendix Completion for Parametric Specifications with Conditional Equations. ADT 1986
21 Harald Ganzinger, Georg Heeg: Efficient Implementation of the Graphical Input/Output for Smalltalk-80. GI Jahrestagung (1) 1986: 151-164
20 Harald Ganzinger: Nichtprozedurale Sprachen und Probleme bei ihrer Implementierung (Kurzfassung). GI Jahrestagung (1) 1986: 35
1985
19 Harald Ganzinger: Modular first-order specifications of operational semantics. Programs as Data Objects 1985: 82-95
18 Harald Ganzinger, Michael Hanus: Modular Logic Programming of Compilers. SLP 1985: 242-253
17 Harald Ganzinger, Walter Willmertinger: FOAM: A Two-Level Approach to Text Formatting on a Microcomputer System. Softw., Pract. Exper. 15(4): 327-341 (1985)
1984
16EEHarald Ganzinger, Robert Giegerich: Attribute coupled grammars. SIGPLAN Symposium on Compiler Construction 1984: 157-170
1983
15 Harald Ganzinger: Modular Compiler Descriptions based on Abstract Semantic Data Types. ADT 1983
14EEHarald Ganzinger: Modular Compiler Descriptions Based on Abstract Semantic Data Types (Extended Abstract). ICALP 1983: 237-249
13EEHarald Ganzinger: Parameterized Specifications: Parameter Passing and Implementation with Respect to Observability. ACM Trans. Program. Lang. Syst. 5(3): 318-354 (1983)
12 Harald Ganzinger: Increasing Modularity and Language-Independency in Automatically Generated Compilers. Sci. Comput. Program. 3(3): 223-278 (1983)
1982
11 Harald Ganzinger: Parameterized Specifications - Parameterized Passing and Implementation with Respect to Observability. ADT 1982
10EEHarald Ganzinger, Robert Giegerich, Ulrich Möncke, Reinhard Wilhelm: A Truly Generative Semantics-Directed Compiler Generator. SIGPLAN Symposium on Compiler Construction 1982: 172-184
1981
9 Harald Ganzinger: Description of Parameterized Compiler Modules. GI Jahrestagung 1981: 11-19
8 Harald Ganzinger: Programs as Transformations of Algebraic Theories (Extended Abstract). GI Jahrestagung 1981: 32-40
1980
7EEHarald Ganzinger: Transforming denotational semantics into practical attribute grammars. Semantics-Directed Compiler Generation 1980: 1-69
1979
6 Harald Ganzinger: An Approach to the Derivation of Compiler Descrition Concepts from the Mathematical Semantics Concept. GI Jahrestagung 1979: 206-217
5 Harald Ganzinger: On Storage Optimization for Automatically Generated Compilers. Theoretical Computer Science 1979: 132-141
1977
4 Harald Ganzinger, Knut Ripken, Reinhard Wilhelm: Automatic Generation of Optimizing Multipass Compilers. IFIP Congress 1977: 535-540
1976
3 Harald Ganzinger: Darstellung der Artanpassung in höheren Programmiersprachen durch Repräsentation von Gruppen. Fachtagung über Programmiersprachen 1976: 194-202
2 Reinhard Wilhelm, Knut Ripken, Joachim Ciesinger, Harald Ganzinger, Walter Lahner, R. Nollmann: Design Evaluation of the Compiler Generating System MUGI. ICSE 1976: 571-576
1975
1 Harald Ganzinger, Reinhard Wilhelm: Verschränkung von Compiler-Moduln. GI Jahrestagung 1975: 654-665

Coauthor Index

1Leo Bachmair [35] [36] [39] [41] [44] [45] [47] [48] [49] [50] [51] [52] [53] [54] [55] [56] [64] [65] [66] [78]
2David A. Basin [57] [77]
3Hubert Baumeister [25]
4Hubert Bertling [25] [28] [30] [33] [46]
5Joachim Ciesinger [2]
6Véronique Cortier [71]
7Robert Giegerich [10] [16] [24]
8George Hagen [92]
9Michael Hanus [18]
10Georg Heeg [21]
11Thomas Hillenbrand [88]
12Ullrich Hustadt [67]
13Florent Jacquemard [68] [71] [75]
14Neil D. Jones [23]
15Christoph M. Kirsch (Christoph Meyer) [62] [67] [70]
16Konstantin Korovin [86] [91] [95]
17Walter Lahner [2]
18Christopher Lynch [44] [56]
19David A. McAllester [73] [82] [84]
20Ulrich Möncke [10]
21Robert Nieuwenhuis [46] [72] [83] [89] [92]
22Pilar Nivela [83] [89]
23Hans de Nivelle [69]
24R. Nollmann [2]
25Albert Oliveras [92]
26Fernando Orejas [46]
27Knut Ripken [2] [4]
28Renate Schäfers [28] [30] [34] [46]
29Renate A. Schmidt [67]
30Peter H. Schmitt [63]
31Jörg H. Siekmann [63]
32Wayne Snyder [44] [56]
33Viorica Sofronie-Stokkermans (Viorica Sofronie) [76] [90] [94]
34Jürgen Stuber [43] [53] [87] [93]
35Cesare Tinelli [92]
36Margus Veanes [68] [70] [71] [75]
37Andrei Voronkov [65] [73]
38Uwe Waldmann [42] [45] [47] [48] [50] [59] [88] [90] [94]
39Christoph Weidenbach [62]
40Reinhard Wilhelm [1] [2] [4] [10]
41Walter Willmertinger [17]

Colors in the list of coauthors

Copyright © Tue Nov 3 08:52:44 2009 by Michael Ley (ley@uni-trier.de)