default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDHarald Ganzinger
Person information
- affiliation: Max Planck Institute for Informatics, Saarbrücken, Germany
- award (2004): Herbrand Award
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
2000 – 2009
- 2006
[j19]Harald Ganzinger, Viorica Sofronie-Stokkermans, Uwe Waldmann:
Modular proof systems for partial functions with Evans equality. Inf. Comput. 204(10): 1453-1492 (2006)- [c76]Harald Ganzinger, Konstantin Korovin:
Theory Instantiation. LPAR 2006: 497-511 - 2005
- [j18]Harald Ganzinger, Jürgen Stuber:
Superposition with equivalence reasoning and delayed clause normal form transformation. Inf. Comput. 199(1-2): 3-23 (2005) - 2004
- [j17]Harald Ganzinger, Robert Nieuwenhuis
, Pilar Nivela:
Fast Term Indexing with Coded Context Trees. J. Autom. Reason. 32(2): 103-120 (2004) - [c75]Harald Ganzinger, Viorica Sofronie-Stokkermans, Uwe Waldmann:
Modular Proof Systems for Partial Functions with Weak Equality. IJCAR 2004: 168-182 - [c74]Harald Ganzinger, George Hagen, Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli:
DPLL( T): Fast Decision Procedures. CAV 2004: 175-188 - [c73]Harald Ganzinger, Konstantin Korovin:
Integrating Equational Reasoning into Instantiation-Based Theorem Proving. CSL 2004: 71-84 - 2003
- [c72]Harald Ganzinger, Thomas Hillenbrand, Uwe Waldmann:
Superposition Modulo a Shostak Theory. CADE 2003: 182-196 - [c71]Harald Ganzinger, Jürgen Stuber:
Superposition with Equivalence Reasoning and Delayed Clause Normal Form Transformation. CADE 2003: 335-349 - [c70]Harald Ganzinger, Konstantin Korovin:
New Directions in Instantiation-Based Theorem Proving. LICS 2003: 55-64 - 2002
- [c69]Harald Ganzinger:
Shostak Light. CADE 2002: 332-346 - [c68]Harald Ganzinger, David A. McAllester:
Logical Algorithms. ICLP 2002: 209-223 - 2001
- [j16]David A. Basin, Harald Ganzinger:
Automated complexity analysis based on ordered resolution. J. ACM 48(1): 70-109 (2001) - [c67]Harald Ganzinger, Robert Nieuwenhuis, Pilar Nivela:
Context Trees. IJCAR 2001: 242-256 - [c66]Harald Ganzinger, David A. McAllester:
A New Meta-complexity Theorem for Bottom-Up Logic Programs. IJCAR 2001: 514-528 - [c65]Harald Ganzinger:
Relating Semantic and Proof-Theoretic Concepts for Polynominal Time Decidability of Uniform Word Problems. LICS 2001: 81-90 - [c64]Harald Ganzinger:
Bottom-Up Deduction with Deletion and Priorities. PADO 2001: 276-278 - [c63]Harald Ganzinger:
Efficient deductive methods for program analysis. POPL 2001: 102-103 - [p2]Leo Bachmair, Harald Ganzinger:
Resolution Theorem Proving. Handbook of Automated Reasoning 2001: 19-99 - 2000
- [j15]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) - [c62]Harald Ganzinger, Viorica Sofronie-Stokkermans:
Chaining Techniques for Automated Theorem Proving in Many-Valued Logics. ISMVL 2000: 337-344
1990 – 1999
- 1999
- [c61]Harald Ganzinger, Robert Nieuwenhuis:
Constraints and Theorem Proving. CCL 1999: 159-201 - [c60]Véronique Cortier, Harald Ganzinger, Florent Jacquemard, Margus Veanes:
Decidable Fragments of Simultaneous Rigid Reachability. ICALP 1999: 250-260 - [c59]Harald Ganzinger, Christoph Meyer, Margus Veanes:
The Two-Variable Guarded Fragment with Transitive Relations. LICS 1999: 24-34 - [c58]Harald Ganzinger, Hans de Nivelle:
A Superposition Decision Procedure for the Guarded Fragment with Equality. LICS 1999: 295-303 - [e6]Harald Ganzinger:
Automated Deduction - CADE-16, 16th International Conference on Automated Deduction, Trento, Italy, July 7-10, 1999, Proceedings. Lecture Notes in Computer Science 1632, Springer 1999, ISBN 3-540-66222-7 [contents] - [e5]Harald Ganzinger, David A. McAllester, Andrei Voronkov:
Logic Programming and Automated Reasoning, 6th International Conference, LPAR'99, Tbilisi, Georgia, September 6-10, 1999, Proceedings. Lecture Notes in Computer Science 1705, Springer 1999, ISBN 3-540-66492-0 [contents] - 1998
- [j14]Leo Bachmair, Harald Ganzinger:
Ordered Chaining Calculi for First-Order Theories of Transitive Relations. J. ACM 45(6): 1007-1049 (1998) - [j13]Harald Ganzinger, Jörg H. Siekmann, Peter H. Schmitt:
Wohin geht die automatische Deduktion? Künstliche Intell. 12(4): 33-37 (1998) - [c57]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 - [c56]Harald Ganzinger, Florent Jacquemard, Margus Veanes:
Rigid Reachability. ASIAN 1998: 4-21 - [c55]Leo Bachmair, Harald Ganzinger:
Strict Basic Superposition. CADE 1998: 160-174 - [c54]Leo Bachmair, Harald Ganzinger, Andrei Voronkov:
Elimination of Equality via Transformation with Ordering Constraints. CADE 1998: 175-190 - 1997
- [c53]Harald Ganzinger, Christoph Meyer, Christoph Weidenbach:
Soft Typing for Ordered Resolution. CADE 1997: 321-335 - 1996
- [c52]Harald Ganzinger:
Saturation-Based Theorem Proving: Past Successes and Future Potential (Abstract). CADE 1996: 1 - [c51]Harald Ganzinger, Uwe Waldmann:
Theorem Proving in Cancellative Abelian Monoids (Extended Abstract). CADE 1996: 388-402 - [c50]Harald Ganzinger:
Saturation-Based Theorem Proving (Abstract). ICALP 1996: 1-3 - [c49]David A. Basin, Harald Ganzinger:
Complexity Analysis Based on Ordered Resolution. LICS 1996: 456-465 - [e4]Harald Ganzinger:
Rewriting Techniques and Applications, 7th International Conference, RTA-96, New Brunswick, NJ, USA, July 27-30, 1996, Proceedings. Lecture Notes in Computer Science 1103, Springer 1996, ISBN 3-540-61464-8 [contents] - 1995
- [j12]Leo Bachmair, Harald Ganzinger, Christopher Lynch, Wayne Snyder:
Basic Paramodulation. Inf. Comput. 121(2): 172-192 (1995) - [c48]Harald Ganzinger:
Redundancy and Saturation. UNIF 1995: 27 - 1994
- [j11]Leo Bachmair, Harald Ganzinger, Uwe Waldmann:
Refutational Theorem Proving for Hierarchic First-Order Theories. Appl. Algebra Eng. Commun. Comput. 5: 193-212 (1994) - [j10]Leo Bachmair, Harald Ganzinger:
Rewrite-Based Equational Theorem Proving with Selection and Simplification. J. Log. Comput. 4(3): 217-247 (1994) - [c47]Leo Bachmair, Harald Ganzinger:
Ordered Chaining for Total Orderings. CADE 1994: 435-450 - [c46]Leo Bachmair, Harald Ganzinger:
Buchberger's Algorithm: A Constraint-Based Completion Procedure. CCL 1994: 285-301 - [c45]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 - [c44]Leo Bachmair, Harald Ganzinger:
Associative-Commutative Superposition. CTRS 1994: 1-14 - [c43]Leo Bachmair, Harald Ganzinger:
Rewrite Techniques for Transitive Relations. LICS 1994: 384-393 - 1993
- [c42]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 - [c41]Leo Bachmair, Harald Ganzinger, Uwe Waldmann:
Set Constraints are the Monadic Class. LICS 1993: 75-83 - [c40]Hubert Bertling, Harald Ganzinger, Renate Schäfers, Robert Nieuwenhuis, Fernando Orejas:
Program Development: Completion Subsystem. PROSPECTRA Book 1993: 460-494 - 1992
- [j9]Harald Ganzinger:
Konferenzbericht LICS '92. Künstliche Intell. 6(3): 51 (1992) - [c39]Leo Bachmair, Harald Ganzinger, Uwe Waldmann:
Theorem Proving for Hierarchic First-Order Theories. ALP 1992: 420-434 - [c38]Leo Bachmair, Harald Ganzinger, Christopher Lynch, Wayne Snyder:
Basic Paramodulation and Superposition. CADE 1992: 462-476 - [c37]Harald Ganzinger, Jürgen Stuber:
Inductive Theorem Proving by Consistency for First-Order Clauses. CTRS 1992: 226-241 - [c36]Harald Ganzinger, Uwe Waldmann:
Termination Proofs of Well-Moded Logic Programs via Conditional Rewrite Systems. CTRS 1992: 430-437 - [c35]Leo Bachmair, Harald Ganzinger:
Non-Clausal Resolution and Superposition with Selection and Redundancy Criteria. LPAR 1992: 273-284 - [p1]Harald Ganzinger, Jürgen Stuber:
Inductive Theorem Proving by Consistency for First-Order Clauses. Informatik 1992: 441-461 - [e3]Johannes Buchmann, Harald Ganzinger, Wolfgang J. Paul:
Informatik, Festschrift zum 60. Geburtstag von Günter Hotz. Teubner-Texte zur Informatik 1, Teubner / Springer 1992, ISBN 978-3-8154-2033-1 [contents] - 1991
- [j8]Harald Ganzinger:
A Completion Procedure for Conditional Equations. J. Symb. Comput. 11(1/2): 51-81 (1991) - [j7]Harald Ganzinger:
Order-Sorted Completion: The Many-Sorted Way. Theor. Comput. Sci. 89(1): 3-32 (1991) - [c34]Leo Bachmair, Harald Ganzinger:
Perfect Model Semantics for Logic Programs with Equality. ICLP 1991: 645-659 - 1990
- [c33]Leo Bachmair, Harald Ganzinger:
On Restrictions of Ordered Paramodulation with Simplification. CADE 1990: 427-441 - [c32]Leo Bachmair, Harald Ganzinger:
Completion of First-Order Clauses with Equality by Strict Superposition (Extended Abstract). CTRS 1990: 162-180 - [c31]Harald Ganzinger, Renate Schäfers:
System Support for Modular Order-Sorted Horn Clause Specifications. ICSE 1990: 150-159
1980 – 1989
- 1989
- [c30]Hubert Bertling, Harald Ganzinger:
Completion-Time Optimization of Rewrite-Time Goal Solving. RTA 1989: 45-58 - [c29]Harald Ganzinger:
Order-Sorted Completion: The Many-Sorted Way (Extended Abstract). TAPSOFT, Vol.1 1989: 244-258 - 1988
- [c28]Hubert Bertling, Harald Ganzinger, Renate Schäfers:
CEC: A System for the Completion of Conditional Equational Specifications. ESOP 1988: 378-379 - [e2]Harald Ganzinger:
ESOP '88, 2nd European Symposium on Programming, Nancy, France, March 21-24, 1988, Proceedings. Lecture Notes in Computer Science 300, Springer 1988, ISBN 3-540-19027-9 [contents] - 1987
- [j6]Harald Ganzinger, Robert Giegerich:
A note on termination in combinatiosn of heterogeneous term rewriting systems. Bull. EATCS 31: 22-27 (1987) - [j5]Hubert Baumeister, Harald Ganzinger, Georg Heeg, Michael Rüger:
Smalltalk-80. it Inf. Technol. 29(4): 241-251 (1987) - [c27]Harald Ganzinger:
Completion with History-Dependent Complexities for Generated Equations. ADT 1987: 73-91 - [c26]Harald Ganzinger:
A Completion Procedure for Conditional Equations. CTRS 1987: 62-83 - [c25]Hubert Bertling, Harald Ganzinger, Renate Schäfers:
A Systems for the Completion of Conditional Equational Specifications. CTRS 1987: 249-250 - [c24]Harald Ganzinger:
Ground Term Confluence in Parametric Conditional Equational Specifications. STACS 1987: 286-298 - [c23]Hubert Bertling, Harald Ganzinger, Hubert Baumeister:
CEC (Conditional Equations Completion). STACS 1987: 470 - 1986
- [c22]Harald Ganzinger:
Knuth-Bendix Completion for Parametric Specifications with Conditional Equations. ADT 1986 - [c21]Harald Ganzinger:
Nichtprozedurale Sprachen und Probleme bei ihrer Implementierung (Kurzfassung). GI Jahrestagung (1) 1986: 35 - [c20]Harald Ganzinger, Georg Heeg:
Efficient Implementation of the Graphical Input/Output for Smalltalk-80. GI Jahrestagung (1) 1986: 151-164 - [e1]Harald Ganzinger, Neil D. Jones:
Programs as Data Objects, Proceedings of a Workshop, Copenhagen, Denmark, October 17-19, 1985. Lecture Notes in Computer Science 217, Springer 1986, ISBN 3-540-16446-4 [contents] - 1985
- [j4]Harald Ganzinger, Walter Willmertinger:
FOAM: A Two-Level Approach to Text Formatting on a Microcomputer System. Softw. Pract. Exp. 15(4): 327-341 (1985) - [c19]Harald Ganzinger:
Modular first-order specifications of operational semantics. Programs as Data Objects 1985: 82-95 - [c18]Harald Ganzinger, Michael Hanus:
Modular Logic Programming of Compilers. SLP 1985: 242-253 - 1984
- [c17]Harald Ganzinger, Robert Giegerich:
Attribute coupled grammars. SIGPLAN Symposium on Compiler Construction 1984: 157-170 - 1983
- [j3]Harald Ganzinger:
Increasing Modularity and Language-Independency in Automatically Generated Compilers. Sci. Comput. Program. 3(3): 223-278 (1983) - [j2]Harald Ganzinger:
Parameterized Specifications: Parameter Passing and Implementation with Respect to Observability. ACM Trans. Program. Lang. Syst. 5(3): 318-354 (1983) - [c16]Harald Ganzinger:
Modular Compiler Descriptions based on Abstract Semantic Data Types. ADT 1983 - [c15]Harald Ganzinger:
Modular Compiler Descriptions Based on Abstract Semantic Data Types (Extended Abstract). ICALP 1983: 237-249 - 1982
- [c14]Harald Ganzinger:
Parameterized Specifications - Parameterized Passing and Implementation with Respect to Observability. ADT 1982 - [c13]Harald Ganzinger:
Denotational Semantics for Languages with Modules. Formal Description of Programming Concepts 1982: 3-24 - [c12]Harald Ganzinger, Robert Giegerich, Ulrich Möncke, Reinhard Wilhelm:
A Truly Generative Semantics-Directed Compiler Generator. SIGPLAN Symposium on Compiler Construction 1982: 172-184 - 1981
- [c11]Harald Ganzinger:
Description of Parameterized Compiler Modules. GI Jahrestagung 1981: 11-19 - [c10]Harald Ganzinger:
Programs as Transformations of Algebraic Theories (Extended Abstract). GI Jahrestagung 1981: 32-40 - 1980
- [j1]Harald Ganzinger, Knut Ripken:
Operator identification in ADA: formal specification, complexity, and concrete implementation. ACM SIGPLAN Notices 15(2): 30-42 (1980) - [c9]Harald Ganzinger:
Transforming denotational semantics into practical attribute grammars. Semantics-Directed Compiler Generation 1980: 1-69
1970 – 1979
- 1979
- [c8]Harald Ganzinger:
An Approach to the Derivation of Compiler Descrition Concepts from the Mathematical Semantics Concept. GI Jahrestagung 1979: 206-217 - [c7]Harald Ganzinger:
On Storage Optimization for Automatically Generated Compilers. Theoretical Computer Science 1979: 132-141 - 1978
- [b1]Harald Ganzinger:
Optimierende Erzeugung von Übersetzerteilen aus implementierungsorientierten Sprachbeschreibungen. Technical University Munich, Germany, 1978, pp. 1-30 - 1977
- [c6]Harald Ganzinger, Knut Ripken, Reinhard Wilhelm:
Automatic Generation of Optimizing Multipass Compilers. IFIP Congress 1977: 535-540 - 1976
- [c5]Ralph E. Griswold, Harald Ganzinger, Bill P. Buckles, G. C. Hintze, Ken De Jong:
SIGPLAN(Paper Session). ACM Annual Conference 1976: 409 - [c4]Harald Ganzinger, Knut Ripken, Reinhard Wilhelm:
MUG1 - an incremental compiler-compiler. ACM Annual Conference 1976: 415-418 - [c3]Reinhard Wilhelm, Knut Ripken, Joachim Ciesinger, Harald Ganzinger, Walter Lahner, R. Nollmann:
Design Evaluation of the Compiler Generating System MUGI. ICSE 1976: 571-576 - [c2]Harald Ganzinger:
Darstellung der Artanpassung in höheren Programmiersprachen durch Repräsentation von Gruppen. Fachtagung über Programmiersprachen 1976: 194-202 - 1975
- [c1]Harald Ganzinger, Reinhard Wilhelm:
Verschränkung von Compiler-Moduln. GI Jahrestagung 1975: 654-665
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
, 
, and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from 
.
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-05-02 21:02 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
