Harald Ganzinger

Publication Activity (10 Years)

Years Active: 1975-2006
Publications (10 Years): 0

Technical University Munich, Germany (PHD)

Education History

Technical University Munich, Germany

PHD

Publications

Harald Ganzinger, Konstantin Korovin
Theory Instantiation. LPAR (2006)
Harald Ganzinger, Viorica Sofronie-Stokkermans, Uwe Waldmann
Modular proof systems for partial functions with Evans equality. Inf. Comput. 204 (10) (2006)
Harald Ganzinger, Jürgen Stuber
Superposition with equivalence reasoning and delayed clause normal form transformation. Inf. Comput. 199 (1-2) (2005)
Harald Ganzinger, Konstantin Korovin
Integrating Equational Reasoning into Instantiation-Based Theorem Proving. CSL (2004)
Harald Ganzinger, Viorica Sofronie-Stokkermans, Uwe Waldmann
Modular Proof Systems for Partial Functions with Weak Equality. IJCAR (2004)
Harald Ganzinger, Robert Nieuwenhuis, Pilar Nivela
Fast Term Indexing with Coded Context Trees. J. Autom. Reason. 32 (2) (2004)
Harald Ganzinger, George Hagen, Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli
DPLL( T): Fast Decision Procedures. CAV (2004)
Harald Ganzinger, Thomas Hillenbrand, Uwe Waldmann
Superposition Modulo a Shostak Theory. CADE (2003)
Harald Ganzinger, Konstantin Korovin
New Directions in Instantiation-Based Theorem Proving. LICS (2003)
Harald Ganzinger, Jürgen Stuber
Superposition with Equivalence Reasoning and Delayed Clause Normal Form Transformation. CADE (2003)
Harald Ganzinger
Shostak Light. CADE (2002)
Harald Ganzinger, David A. McAllester
Logical Algorithms. ICLP (2002)
Harald Ganzinger
Bottom-Up Deduction with Deletion and Priorities. PADO (2001)
David A. Basin, Harald Ganzinger
Automated complexity analysis based on ordered resolution. J. ACM 48 (1) (2001)
Harald Ganzinger, David A. McAllester
A New Meta-complexity Theorem for Bottom-Up Logic Programs. IJCAR (2001)
Harald Ganzinger
Relating Semantic and Proof-Theoretic Concepts for Polynominal Time Decidability of Uniform Word Problems. LICS (2001)
Harald Ganzinger, Robert Nieuwenhuis, Pilar Nivela
Context Trees. IJCAR (2001)
Harald Ganzinger
Efficient deductive methods for program analysis. POPL (2001)
Harald Ganzinger, Viorica Sofronie-Stokkermans
Chaining Techniques for Automated Theorem Proving in Many-Valued Logics. ISMVL (2000)
Harald Ganzinger, Florent Jacquemard, Margus Veanes
Rigid Reachability, The Non-Symmetric Form of Rigid E-Unification. Int. J. Found. Comput. Sci. 11 (1) (2000)
Harald Ganzinger, Robert Nieuwenhuis
Constraints and Theorem Proving. CCL (1999)
Véronique Cortier, Harald Ganzinger, Florent Jacquemard, Margus Veanes
Decidable Fragments of Simultaneous Rigid Reachability. ICALP (1999)
Harald Ganzinger, Christoph Meyer, Margus Veanes
The Two-Variable Guarded Fragment with Transitive Relations. LICS (1999)
Harald Ganzinger, Hans de Nivelle
A Superposition Decision Procedure for the Guarded Fragment with Equality. LICS (1999)
Leo Bachmair, Harald Ganzinger, Andrei Voronkov
Elimination of Equality via Transformation with Ordering Constraints. CADE (1998)
Harald Ganzinger, Jörg H. Siekmann, Peter H. Schmitt
Wohin geht die automatische Deduktion? Künstliche Intell. 12 (4) (1998)
Leo Bachmair, Harald Ganzinger
Ordered Chaining Calculi for First-Order Theories of Transitive Relations. J. ACM 45 (6) (1998)
Harald Ganzinger, Florent Jacquemard, Margus Veanes
Rigid Reachability. ASIAN (1998)
Harald Ganzinger, Ullrich Hustadt, Christoph Meyer, Renate A. Schmidt
A Resolution-Based Decision Procedure for Extensions of K4. Advances in Modal Logic (1998)
Leo Bachmair, Harald Ganzinger
Strict Basic Superposition. CADE (1998)
Harald Ganzinger, Christoph Meyer, Christoph Weidenbach
Soft Typing for Ordered Resolution. CADE (1997)
Harald Ganzinger
Saturation-Based Theorem Proving (Abstract). ICALP (1996)
Harald Ganzinger, Uwe Waldmann
Theorem Proving in Cancellative Abelian Monoids (Extended Abstract). CADE (1996)
David A. Basin, Harald Ganzinger
Complexity Analysis Based on Ordered Resolution. LICS (1996)
Harald Ganzinger
Saturation-Based Theorem Proving: Past Successes and Future Potential (Abstract). CADE (1996)
Harald Ganzinger
Redundancy and Saturation. UNIF (1995)
Leo Bachmair, Harald Ganzinger, Christopher Lynch, Wayne Snyder
Basic Paramodulation Inf. Comput. 121 (2) (1995)
Leo Bachmair, Harald Ganzinger
Rewrite-Based Equational Theorem Proving with Selection and Simplification. J. Log. Comput. 4 (3) (1994)
Leo Bachmair, Harald Ganzinger
Associative-Commutative Superposition. CTRS (1994)
Leo Bachmair, Harald Ganzinger
Buchberger's Algorithm: A Constraint-Based Completion Procedure. CCL (1994)
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)
Leo Bachmair, Harald Ganzinger
Rewrite Techniques for Transitive Relations LICS (1994)
Leo Bachmair, Harald Ganzinger, Uwe Waldmann
Refutational Theorem Proving for Hierarchic First-Order Theories. Appl. Algebra Eng. Commun. Comput. 5 (1994)
Leo Bachmair, Harald Ganzinger
Ordered Chaining for Total Orderings. CADE (1994)
Leo Bachmair, Harald Ganzinger, Uwe Waldmann
Set Constraints are the Monadic Class LICS (1993)
Hubert Bertling, Harald Ganzinger, Renate Schäfers, Robert Nieuwenhuis, Fernando Orejas
Program Development: Completion Subsystem. PROSPECTRA Book (1993)
Leo Bachmair, Harald Ganzinger, Uwe Waldmann
Superposition with Simplification as a Desision Procedure for the Monadic Class with Equality. Kurt Gödel Colloquium (1993)
Harald Ganzinger, Jürgen Stuber
Inductive Theorem Proving by Consistency for First-Order Clauses. CTRS (1992)
Leo Bachmair, Harald Ganzinger
Non-Clausal Resolution and Superposition with Selection and Redundancy Criteria. LPAR (1992)
Harald Ganzinger
Konferenzbericht LICS '92. Künstliche Intell. 6 (3) (1992)
Leo Bachmair, Harald Ganzinger, Uwe Waldmann
Theorem Proving for Hierarchic First-Order Theories. ALP (1992)
Leo Bachmair, Harald Ganzinger, Christopher Lynch, Wayne Snyder
Basic Paramodulation and Superposition. CADE (1992)
Harald Ganzinger, Uwe Waldmann
Termination Proofs of Well-Moded Logic Programs via Conditional Rewrite Systems. CTRS (1992)
Leo Bachmair, Harald Ganzinger
Perfect Model Semantics for Logic Programs with Equality. ICLP (1991)
Harald Ganzinger
Order-Sorted Completion: The Many-Sorted Way. Theor. Comput. Sci. 89 (1) (1991)
Harald Ganzinger
A Completion Procedure for Conditional Equations. J. Symb. Comput. 11 (1/2) (1991)
Harald Ganzinger, Renate Schäfers
System Support for Modular Order-Sorted Horn Clause Specifications. ICSE (1990)
Leo Bachmair, Harald Ganzinger
Completion of First-Order Clauses with Equality by Strict Superposition (Extended Abstract). CTRS (1990)
Leo Bachmair, Harald Ganzinger
On Restrictions of Ordered Paramodulation with Simplification. CADE (1990)
Harald Ganzinger
Order-Sorted Completion: The Many-Sorted Way (Extended Abstract). TAPSOFT, Vol.1 (1989)
Hubert Bertling, Harald Ganzinger
Completion-Time Optimization of Rewrite-Time Goal Solving. RTA (1989)
Hubert Bertling, Harald Ganzinger, Renate Schäfers
CEC: A System for the Completion of Conditional Equational Specifications. ESOP (1988)
Hubert Bertling, Harald Ganzinger, Renate Schäfers
A Systems for the Completion of Conditional Equational Specifications. CTRS (1987)
Harald Ganzinger
A Completion Procedure for Conditional Equations. CTRS (1987)
Harald Ganzinger
Ground Term Confluence in Parametric Conditional Equational Specifications. STACS (1987)
Hubert Baumeister, Harald Ganzinger, Georg Heeg, Michael Rüger
Smalltalk-80. it Inf. Technol. 29 (4) (1987)
Harald Ganzinger
Completion with History-Dependent Complexities for Generated Equations. ADT (1987)
Hubert Bertling, Harald Ganzinger, Hubert Baumeister
CEC (Conditional Equations Completion). STACS (1987)
Harald Ganzinger, Robert Giegerich
A note on termination in combinatiosn of heterogeneous term rewriting systems. Bull. EATCS 31 (1987)
Harald Ganzinger
Nichtprozedurale Sprachen und Probleme bei ihrer Implementierung (Kurzfassung). GI Jahrestagung (1) (1986)
Harald Ganzinger, Georg Heeg
Efficient Implementation of the Graphical Input/Output for Smalltalk-80. GI Jahrestagung (1) (1986)
Harald Ganzinger
Knuth-Bendix Completion for Parametric Specifications with Conditional Equations. ADT (1986)
Harald Ganzinger, Walter Willmertinger
FOAM: A Two-Level Approach to Text Formatting on a Microcomputer System. Softw. Pract. Exp. 15 (4) (1985)
Harald Ganzinger
Modular first-order specifications of operational semantics. Programs as Data Objects (1985)
Harald Ganzinger, Michael Hanus
Modular Logic Programming of Compilers. SLP (1985)
Harald Ganzinger, Robert Giegerich
Attribute coupled grammars. SIGPLAN Symposium on Compiler Construction (1984)
Harald Ganzinger
Modular Compiler Descriptions Based on Abstract Semantic Data Types (Extended Abstract). ICALP (1983)
Harald Ganzinger
Parameterized Specifications: Parameter Passing and Implementation with Respect to Observability. ACM Trans. Program. Lang. Syst. 5 (3) (1983)
Harald Ganzinger
Modular Compiler Descriptions based on Abstract Semantic Data Types. ADT (1983)
Harald Ganzinger
Increasing Modularity and Language-Independency in Automatically Generated Compilers. Sci. Comput. Program. 3 (3) (1983)
Harald Ganzinger
Denotational Semantics for Languages with Modules. Formal Description of Programming Concepts (1982)
Harald Ganzinger, Robert Giegerich, Ulrich Möncke, Reinhard Wilhelm
A Truly Generative Semantics-Directed Compiler Generator. SIGPLAN Symposium on Compiler Construction (1982)
Harald Ganzinger
Parameterized Specifications - Parameterized Passing and Implementation with Respect to Observability. ADT (1982)
Harald Ganzinger
Description of Parameterized Compiler Modules. GI Jahrestagung (1981)
Harald Ganzinger
Programs as Transformations of Algebraic Theories (Extended Abstract). GI Jahrestagung (1981)
Harald Ganzinger, Knut Ripken
Operator identification in ADA: formal specification, complexity, and concrete implementation. ACM SIGPLAN Notices 15 (2) (1980)
Harald Ganzinger
Transforming denotational semantics into practical attribute grammars. Semantics-Directed Compiler Generation (1980)
Harald Ganzinger
An Approach to the Derivation of Compiler Descrition Concepts from the Mathematical Semantics Concept. GI Jahrestagung (1979)
Harald Ganzinger
On Storage Optimization for Automatically Generated Compilers. Theoretical Computer Science (1979)
Harald Ganzinger, Knut Ripken, Reinhard Wilhelm
Automatic Generation of Optimizing Multipass Compilers. IFIP Congress (1977)
Ralph E. Griswold, Harald Ganzinger, Bill P. Buckles, G. C. Hintze, Ken De Jong
SIGPLAN(Paper Session). ACM Annual Conference (1976)
Harald Ganzinger, Knut Ripken, Reinhard Wilhelm
MUG1 - an incremental compiler-compiler. ACM Annual Conference (1976)
Harald Ganzinger
Darstellung der Artanpassung in höheren Programmiersprachen durch Repräsentation von Gruppen. Fachtagung über Programmiersprachen (1976)
Reinhard Wilhelm, Knut Ripken, Joachim Ciesinger, Harald Ganzinger, Walter Lahner, R. Nollmann
Design Evaluation of the Compiler Generating System MUGI. ICSE (1976)
Harald Ganzinger, Reinhard Wilhelm
Verschränkung von Compiler-Moduln. GI Jahrestagung (1975)

Harald Ganzinger.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Harald Ganzinger